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.

  • 10
    I'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
  • 3
    Federico 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
  • 2
    Could 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
  • 1
    For 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
  • 6
    I'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
  • @KevinBuzzard, the rules and guidelines are clear enough....but the norms are unclear, and which rules and guidelines the community wants to uphold is unclear. I find that this unclarity is also unfriendly and unwise. But many active users prefer not to codify new guidelines, and prefer to disregard things already codified. – Matt F. Oct 19 at 2:33

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.

  • 1
    xenaproject.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
  • 5
    Here is some background. We are a loose-knit 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
  • 4
    The 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
  • 1
    I 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
  • 6
    I 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 Feit-Thomson 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
  • 1
    hmm, 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 advertising---appropriate 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 even-handed. – Kevin Buzzard Sep 24 at 7:48
  • 1
    IMHO 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/2018-55-04/S0273-0979-2018-01616-9/… – 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

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.

  • It is an improvement, but I still think that there are some elements of advertising left that I don't like. I would strike out the parts that start with "My own experience...", "For example..." and "If you want to understand...", up to the end of these paragraphs. The first one in particular. They are unnecessarily personal (they sound a bit like "here is my amazing experience with Lean"), and contain various invitations to learn more about Lean and join the community. In most cases, just a link is enough of a pointer; there is no need to invite people to click on it. – Federico Poloni Oct 18 at 16:44
  • Another point to consider is that the question could have been formulated for a general theorem prover: "Which mathematical objects would you like to see formally defined in a theorem prover". – Federico Poloni Oct 18 at 16:46
  • 2
    Federico, you seem to take a hard line with respect to the expression of anything personal, and in another meta post you questioned the good faith of others, accusing them of misusing the site to garner attention for themselves. I am disinclined to remove "if you want to understand better" because that could be information for people who want to understand what sort of answer might be appropriate. The "for example" could be changed to "for example, formalising the definition of scheme [linked]" [end of paragraph], but the change in the wording of that sentence begins to sound finicky to me. – Todd Trimble Oct 19 at 8:43
  • As for your second comment, I don't think that's what OP wants to ask. This is a Lean-specific question. What concepts might people want to see that are not yet in Lean, etc. As for your first objection ("my own experience") -- in general I think that kind of personal expression should be allowed, and that authors should be allowed some autonomy and not have to submit entirely to the editorial opinions of others. I'll think about toning down "my own experience" slightly, but some tolerance for personal expression would, I think, be helpful. – Todd Trimble Oct 19 at 8:52
  • 1
    My main objection is not to the personal statements, but to the repeated invitations to learn more about the project. This is just my opinion, anyway (provided on your request). I will respect your final decision on what to with this question. – Federico Poloni Oct 19 at 9:10
  • @FedericoPoloni Indeed I did request your response, and should have thanked you for it before. I'd like to venture one idea I had: think of Lean or other proof assistant software as itself close to being a mathematical object. (At its core it and others are based on dependent type theory. Cf. also en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence where "proofs" and "programs" are identified.) If it really were a case of proprietary software, I'd agree there'd be a problem, but here we can just think them as mathematical frameworks. Might this ameliorate the advertising aspect? – Todd Trimble Oct 19 at 14:00
  • No, not in my view. I think this level of advocacy for a mathematical theory would be equally off-topic on this site. As far as I understand Lean is open source, and I did not see advertising for proprietary software as a significant part of the issue. Anyway, thanks for your efforts in understanding my point of view. I am sorry I am causing you to spend so much time on this issue. – Federico Poloni Oct 19 at 15:30

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .