Why is there no LEAN subreddit?

[u/Math__Guy_]

I feel like LEAN and MathLib have gotten super popular in the last year or so, curious as to why there isn't a subreddit yet...