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.

10I'm happy either way. I used to be very active here and I had an intuitive feeling for what I thought a good / bad question looked like. I no longer have that feeling and the community has changed as well. As anyone who looks through the edit history will see, after all the background stuff was deleted I wrote a blog post saying roughly the same thing, and added a link from the MO post to the blog post. Now the original post is back and we have a data point of someone saying they found it valuable. Ultimately I would like to abide by the rules and guidelines, but I no longer know them. – Kevin Buzzard Sep 22 at 12:47

3Federico thought that a lot of the discussion looked like advertising for Lean. That's not how it struck me, but I see now that Federico has posted an answer. – Todd Trimble♦ Sep 22 at 13:26

2Could one of the users who disagree with me please write something more detailed than "I thought it was OK"? – Federico Poloni Sep 22 at 16:05

I feel that the removal of the section is too drastic, but changes to it are in order, see my answer... – Dima Pasechnik Sep 22 at 18:39

1For people who want to see it, here's Kevin's blog post: xenaproject.wordpress.com/2018/09/22/… (EDIT: which I see now he gave in a comment to Frederico's answer) – David Roberts Sep 23 at 2:23

5I'm sure that Kevin Buzzard is proud to own his question, but it seems like a bad precedent to have people think that MeMO posts can or should name individual posters. Especially since it's currently a hot meta post, how about removing Kevin's name from the title (not necessarily from the post itself)? – LSpice Sep 25 at 11:51
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 tothepoint 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 wellwritten, and you probably like it, but do not let that distract you; it's still offtopic (in my interpretation of the rules).
From the help center:
MathOverflow is not a discussion forum. As a sideeffect of being very good for tothepoint 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.
and, below
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.

1xenaproject.wordpress.com/2018/09/22/…  when you deleted the question I guessed that your thoughts would be what you have written above, and I wrote a blog post. – Kevin Buzzard Sep 22 at 14:18

5Here is some background. We are a looseknit community of mathematicians and computer scientists with a vast amount of synergy. I have strongly argued on the Lean chat that the computer scientists should be devoting a lot more time formalising the mathematics that mathematicians are actually interested in and a lot less time formalising the mathematics which fits best into their theorem provers for whatever reason. What has happened in practice is that we are now formalising the kind of mathematics which the mathematicians among us are interested in e.g. perfectoid spaces. (1/2) – Kevin Buzzard Sep 22 at 14:22

4The original motivation behind the question is that I wanted to get a feeling from a broader community of mathematicians as to the kind of values of X which would make them think "hey! Lean now has X in it!". Already there is discussion on the Lean chat about formalising the statement of the classification of finite simple groups and which goals are actually going to be achievable. That was one of the main aims of the post. Of course another aim is trying to raise the visibility of Lean and maybe of theorem provers in general, and this is because I believe mathematicians need to know! (2/2) – Kevin Buzzard Sep 22 at 14:26

2@KevinBuzzard I think that the question and this motivation are good, and should stay on MO. What I disagree is only the last section, which has no role in the question and is there just to raise the visibility of Lean. MO is a site to ask questions and give answers, not a blog or a news site where you post to get your project known. – Federico Poloni Sep 22 at 14:55

1I put it there in an attempt to show that the "obviously completely impossible task for a 1st year undergraduate" of learning how to formalise mathematics was now much easier than it used to be. I put it there to show that formalisation is now for the normal mathematician. I completely agree that it reads like an advert. I think it is desperately important for the mathematics community to understand it. I understand your point of view. As I already said, I just blogged all the information after you deleted it. I played no role in either the deletion or undeletion and don't know what is best. – Kevin Buzzard Sep 22 at 16:44


6I upvoted this to support my concern that I don't want to see MO overrun with spammy project posts. However, I don't think Kevin Buzzard crossed "the line" (a fuzzy ambiguous thing), and thought his post was just barely acceptable for being a good fit for the community (and in fact contributes to the community for some of the reasons he outlines). Perhaps he gets the benefit for being first, but ... I think if there were a bunch of similar posts that start showing up I would voice concern on meta. But this question, in this particular instance, I think is ok. – Ben Burns Sep 23 at 1:28
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 FeitThomson Odd Order theorem...)

I am open to rewrite suggestions. I am completely happy to strive to comply with what the community thinks is best. As for other systems, I don't see any real reason why all this can't happen in Coq or Mizar but these communities seem to have no growth. I am not an expert in these systems. What I do not understand is why these systems have been round forever but nobody from their communities seems to be targetting recent research level maths  the kind of stuff that makes us tick. They seem to be more concerned with stuff like constructivism which to a mainstream mathematician is very niche. – Kevin Buzzard Sep 22 at 19:41

1hmm, have you heard of en.wikipedia.org/wiki/Univalent_foundations ? Which is a modern research level maths... – Dima Pasechnik Sep 23 at 10:24

Also, while saying "it has been success with undergraduates" is OK, giving names without specifying concrete accomplishments smacks of advertisingappropriate for your own blog, less so for MO, IMHO. – Dima Pasechnik Sep 23 at 10:34

Waitwaitwait  I specifically link to, and name, the achievements of Chris Hughes, who formalised the statements and proofs of Sylow's theorems, and Kenny Lau, who has, modulo existence of algebraic closure of a field (which he is working on), and a construction from local class field theory (which he declared as an axiom), stated the local Langlands conjectures for tori. – Kevin Buzzard Sep 23 at 19:00

I do know about univalent foundations, but I have never used it. Lean uses dependent type theory, which is something else. Lean's type theory is equiconsistent with ZFC + infinitely many inaccessible cardinals. I don't know what the proof strength of most of the other systems is. – Kevin Buzzard Sep 23 at 20:41

Something else than what? This is not actually my area, so I don't really want to argue, but I understand Coq to be also based on dependent type theory. See for instance adam.chlipala.net/papers/CpdtJFR/CpdtJFR.pdf – Todd Trimble♦ Sep 24 at 1:30

@KevinBuzzard the post says "links to their undergrad projects", but does not give links (otherwise, indeed, I should have been more precise, sorry). – Dima Pasechnik Sep 24 at 7:22

My understanding of the way univalent foundations works is that you write it in coq but that you are not allowed to use some of Coq's functionality! On the other hand they add in an extra axiom which is not part of Coq. So I'm not so sure that it's dependent type theory any more. I think people call it homotopy type theory. – Kevin Buzzard Sep 24 at 7:29

2@DimaPasechnik I now see the issue! The original version of the question had many more links in the question. Perhaps during the removal and restoral all those links disappeared. "links to their undergraduate project" used to be links. – Kevin Buzzard Sep 24 at 7:31

OK Dima thanks for pointing this out. I have put some links back, and I have removed a couple of explicit mentions to Lean in some places where "a theorem prover" would do just as well. This is an attempt to make the background a bit more evenhanded. – Kevin Buzzard Sep 24 at 7:48

1IMHO univalence axiom, used in homotopy type theory, is an extension of very bare foundations provided by Coq. Anyhow the following seems nicely written: ams.org/journals/bull/20185504/S027309792018016169/… – Dima Pasechnik Sep 24 at 8:23

Read the first sentence here: ncatlab.org/nlab/show/homotopy+type+theory HoTT is based on intensional dependent type theory, with yes, some more axioms such as univalence. – Todd Trimble♦ Sep 24 at 18:46