Should Kevin Buzzard's Lean question be left in its original state?

Question

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.

Answer 1

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.

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.

Answer 2

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...)

Answer 3

I've had another look at the Lean post, and believe it should be trimmed down. I'll have a go at suggesting edits (which Kevin Buzzard seems to invite in a comment below Dima's answer), after I reproduce the post in its current state as of this writing.

As will be evident, I am not in favor of wholesale removal of the background section. The help center does recommend inclusion of background text where it will help mathematicians understand surrounding context, motivations, what the issues that concern the OP are, etc. Edits are in order where it begins to smack of advertisement or opinion-giving or self-indulgence.

---

(Original post)

The question.

Which mathematical objects would you like to see formally defined in the Lean Theorem Prover?

Examples.

In the current stable version of the Lean Theorem Prover, topological groups have been done, schemes have been done, Noetherian rings got done last month, Noetherian schemes have not yet been done (but are probably not going to be too difficult, if anyone is interested in trying), but complex manifolds have not yet been done. In fact I think we are nearer to perfectoid spaces than complex manifolds -- maybe because algebra is closer to the axioms than analysis. But actually we also have Lebesgue measure (it's differentiability we're not too strong at), and today we got modular forms. There is a sort of an indication of where we are.

What else should we be doing? What should we work on next?

Some background.

The Lean theorem prover is a computer program which can check mathematical proofs which are written in a sufficiently formal mathematical language. You can read my personal thoughts on why I believe this sort of thing is timely and important for the pure mathematics community. Other formal proof verification software exists (Coq, Isabelle, Mizar...). I am very ignorant when it comes to other theorem provers and feel like I would like to see a comparison of where they all are.

Over the last year I have become increasingly interested in Lean's mathematics library, because it contains a bunch of what I as a number theorist regard as "normal mathematics". No issues with constructivism, the axiom of choice, quotients by equivalence relations, the law of the excluded middle or anything. My impression that most mathematicians are not particularly knowledgeable about what can actually be done now with computer proof checkers, and perhaps many have no interest. These paragraphs are an attempt to give an update to the community.

Let's start by getting one thing straight -- formalising deep mathematical proofs is extremely hard. For example, it would cost tens of millions of dollars at least, i.e. many many person-years, to formalize and maintain (a proof is a computer program, and computer programs needs maintaining!) a complete proof of Fermat's Last Theorem in a theorem prover. It would certainly be theoretically possible, but it is not currently clear to me whether any funding bodies are interested in that sort of project.

But formalising deep mathematical objects is really possible nowadays. I formalised the definition of a scheme earlier this year. But here's the funny thing. 15 months ago I had never heard of the Lean Theorem Prover, and I had never used anything like a theorem prover in my life. Then in July 2017 I watched a live stream (thank you Newton Institute!) of Tom Hales' talk in Cambridge, and in particular I saw his answer to Tobias Nipkow's question 48 minutes in. And here we are now, just over a year later, with me half way through perfectoid spaces, integrating Lean into my first year undergraduate teaching, and two of my starting second year Imperial College undergraduate students, Chris Hughes and Kenny Lau, both much better than me at it. The links are to their first year undergraduate projects, one a complete formal proof of Sylow's theorems and the other an almost finished formalization of the local Langlands conjectures for abelian algebraic groups over a p-adic field. It's all open source, we are writing the new Bourbaki in our spare time and I cannot see it stopping. I know many people don't care about Bourbaki, and I know it's not a perfect analogy, but I do care about Bourbaki. I want to know which chapters should get written next, because writing them is something I find really good fun.

But why write Bourbaki in a computer language? Well whether you care or not, I think it's going to happen. Because it's there. Whether it happens in Lean or one of the other systems -- time will tell. Tom Hales' formal abstracts project plans to formalise the statements of new theorems (in Lean) as they come out -- look at his blog to read more about his project. But to formalise the statements of hard theorems you have to formalise the definitions first. Mathematics is built on rigorous definitions. Computers are now capable of understanding many more mathematical definitions than they have ever been told, and I believe that this is mostly because the mathematical community, myself included, just didn't ever realise or care that it was happening. If you're a mathematician, I challenge you to formalise your best theorem in a theorem prover and send it to Tom Hales! If you need hints about how to do that in Lean, come and ask us at the Lean Zulip chat. And if if it turns out that you can't do it because you are missing some definitions, you can put them down here as answers to this big list question.

We are a small but growing community at the Lean prover Zulip chat and I am asking for direction.

---

(And now my suggestions for edits.)

Let's leave the Question and the Examples sections as they are, as these seem not to be in question.

The first paragraph of the Background section seems very appropriate to me: it's informational, and the author should be allowed to say why this is important to him by linking to his blog post. If the author would like to mention briefly that the software is open source, this might be the best place ("The Lean theorem prover is an open source computer program..."). However, I would modify the last sentence

I am very ignorant when it comes to other theorem provers and feel like I would like to see a comparison of where they all are.

to something more like this:

I am unfortunately ignorant when it comes to these other theorem provers; if it seems that I am focusing on Lean to the exclusion of the others, it's only because it's Lean that I have experience with.

(I am removing the bit about "would like to see a comparison" because that should not be construed as part of the question -- presumably answers that go into comparisons would be considered "not an answer", i.e., not relevant.)

I would either remove the second paragraph or replace it with something different. To me it is alluding to some invidious comparisons between Lean and what the author thinks about the other theorem provers out there (as being not well adapted to doing "normal mathematics", presumably, and allegedly overly occupied with "niche concerns" as Kevin opined in a comment). At most I would constrain it to something like

For mathematicians who are worried about being able to understand the formalization, I invite them to take a look at Lean's mathematics library. My own experience suggests that you do not at all have to be a logician or type theorist to begin using this technology (15 months ago I had never heard of the Lean Theorem Prover, and I had never used anything like a theorem prover in my life). Plus, looking over the library may give the reader a better sense of which gaps need filling in Lean.

The next few paragraphs, as I read them, are really (or should be) about clarifying the scope of the question. But they should be trimmed down just to get that across, because as they stand they sort of go on and on. Also, I'm being picky here, but tonally "Let's start with getting one thing straight" sounds a bit like the beginning of a rejoinder in an argument with someone. Here's what I might try instead:

Let's start with saying one thing up front: formalising deep mathematical proofs is extremely hard, time-consuming, and costly. (I estimate it would take upwards of tens of millions of dollars to implement and maintain the code it would take to formalize [huh, did Kevin mean to write 'formalise'? :-)] say the proof of Fermat's last theorem.) Suggestions for that type of huge project is not what I am asking about here.

What is feasible, and what I am largely focused on here, is formalising deep mathematical objects. For example, earlier this year I formalised the definition of a scheme. For some other examples, including some personal experiences I've had in incorporating this sort of project in undergraduate education, please see my blog post.

To put this in a greater context: many of us see ourselves as writing, as our spare time allows, the new Bourbaki in a formalised computer language. (This is bound to happen -- whether in Lean or some other framework, only time will tell.) So you could think of my question as basically asking: which chapters of Bourbaki we should be writing next? But especially with a focus on where they need to start: which key concepts, from chapters to be written, should we emphasise as the next candidates for rigorous formalised definitions? Everything else would be built on that, with hard proofs following in the fullness of time.

(If you want to understand better what exactly would be involved in doing this sort of thing, please feel free to ask the growing community at the Lean prover Zulip chat.)

I think this might go over better, but Kevin and Federico and Neil should let us know what they think about this.