Kevin Buzzard asked this question, which incorporated a long section of background discussion. Federico Poloni removed that section. Yemon Choi commented that he thought the question was OK before this removal. I agree, and plan to put it back in in a moment. We can discuss further here if necessary.
My opinion, posted as an answer here so that it is ready for the downvotes.
The "background" section reads more like a blog post than a question, and I feel it's out of place on this website. You could add a similar section to many questions and topics: with a great introduction and discussion (think one of Terence Tao's blog posts), they probably would attract more interest; but this is not a blog, it's a site for short and to-the-point questions.
That section is not an essential part of the question: the question made perfect sense even after the removal. It's not even, strictly speaking, background material, such as definitions or an introduction. It's just OP's personal views on the topic, and advocacy for Lean. It doesn't help that OP is working directly on the project. He is basically using Mathoverflow's visibility to post something that is not a question, to attract attention to their project. If this was a commercial product, I would not hesitate to label it as spam. I am sure OP is moved only by genuine enthusiasm for this field of research and has no selfish intents, but maybe he got carried away.
I think it would be harmful for this website if all questions looked like this one. But that's just, like, my opinion. If you all want a different MO, I acknowledge that mine is a minority view.
That section is interesting, is well-written, and you probably like it, but do not let that distract you; it's still off-topic (in my interpretation of the rules).
From the help center:
MathOverflow is not a discussion forum. As a side-effect of being very good for to-the-point questions and answers, the Stack Exchange software is bad for discussions and designed to minimize them. There's a place for discussion about mathematics, but it isn't MathOverflow. Blogs and threaded discussion forums are a more appropriate place for discussions.
MathOverflow is not an encyclopedia. MO is a site for questions that have answers. [...] MathOverflow is not the appropriate place to ask somebody to write an expository article for you. If you want somebody to write an article about some subject, you should make a stub on Wikipedia, make a query block on nLab, or make a request on PlanetMath.
The background section sounds a bit too opinionated. I'd welcome it to be toned down a bit, and mention other similar efforts (e.g. the Coq community has a similar, and, I guess, larger, effort going on, including a relatively recent formalisation of Feit-Thomson Odd Order theorem...)