Formalising Mathematics: An Introduction | Hacker News Reader

Formalising Mathematics: An Introduction

xenaproject.wordpress.com

205 pointspanic116 comments

If anyone wants of a concrete reason to formalize mathematics, consider this. The classification of finite simple groups is a major result in mathematics that is a foundation for many others. See https://en.wikipedia.org/wiki/Classification_of_finite_simpl... for more.

However at the time the proof was finishing, people were leaving the field, and the very people who proved it did not feel that their results were checked. They were not confident of the result. And nobody has been able to review the proof.

This began a decades long effort, which is currently incomplete, to produce a second proof that is more understandable. That effort seems to have fizzled out.

So one of the most important results in mathematics in the 20th century does not have a proof that anyone can understand or review. And this is true despite a number of very smart people devoting their entire lives to the subject.

I maintain that no amount of human verification and re-verification will result in my being as confident of this result as I am about most mathematical results that I know. The only way to actually make this into something we should be confident of is to translate the existing proofs to something computer checkable.

> I maintain that no amount of human verification and re-verification will result in my being as confident of this result as I am about most mathematical results that I know. The only way to actually make this into something we should be confident of is to translate the existing proofs to something computer checkable.

Or to indeed find that simpler proof, I suppose?

(Not disagreeing with anything you're saying, just checking - it's a fascinating story that I didn't know about this topic)

I don't understand this area well at all, but I know the existing classification of finite simple groups is very long and detailed.

Wikipedia says

> The proof consists of tens of thousands of pages in several hundred journal articles

and that the second-generation simplified version might possibly run to only 5,000 pages.

5,000 pages of math is easier to understand and/or believe in than tens of thousands of pages, but it's still a pretty daunting amount even for specialists.

Why would it have to be one person? I would assume that the proof can be presented as mostly modular based on compositing results from the related published work

A game to try this out (by Kevin Buzzard, who is participating in this thread and is also the author of this blog post).

https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_gam...

I loved it and have been trying to make some subsequent levels about divisibility.

I played it recently. I spent almost a full day to finish all the worlds and then lost interest afterwards.

I think I had expectations that it would be a lot less ... tedious? Like I was hoping it would be mostly automated except needing hints whenever it got stuck. Much like how the flavor text would hint to you (the human) that you needed to use certain theorems for certain levels.

Instead, it was so low level that you had to do every step of algebra manually with a line of code each. (and to be fair, in the beginning it was necessary because you're developing the usual rules of algebra as you go, but even in the later levels after they tell you about the ring tactic there's still a lot of manual algebra you need to do) The search space seems small enough that even I was just mindlessly spamming rewrite/intro/apply/induction. Why can't a computer automate this completely.

And going in the other direction, I was hoping this would be a good tool to aid in proofwriting. But most of the "proof" I wrote was complete gibberish not meant for human consumption. I think the problem is because the code relies heavily on mutating a context that you can't see without using the lean UI.

Anyway, maybe the number game is just not a good intro to the full capabilities of lean and I am missing the point.

No, I think you have a pretty good grasp of things. In the real world people do use more powerful tactics like ring to skip all the low-level algebraic manipulation (which I personally really enjoyed but can see others finding tedious).

Your point about proof readability applies to interactive theorem provers generally. You can see a tradeoff here between Lean/Coq and more "literate" formal proof languages like TLA+, which has a prover called TLAPS (TLA+ Proof System). TLA+ proofs are written in a hierarchical style Lamport proposed in his paper How to Write a 21st Century Proof[0], and are readable by themselves. The BIG BIG tradeoff here is that when you're writing the proof in TLA+, it's very difficult to know what the prover is "thinking" and why it is stuck. Whereas with interactive provers you know exactly what the prover is "thinking" - the proof consists solely of instructions to manipulate those thoughts which you see on screen at all times! So at this time it seems there's a tradeoff between ease of writing a formal proof and ease of reading a formal proof.

[0] https://www.microsoft.com/en-us/research/publication/write-2...

The algebra was tedious because for example, the very second thing you prove in the tutorial is that addition is associative. If you were teaching this to humans you would then immediately tell them that you now can omit parentheses because you have an algorithm to re-parenthesize however you want.

But instead, for entire rest of the tutorial, you had to manually rewrite every single parenthesis yourself (with syntax that is pretty unergonomic for doing so too).

I guess I found it a little disappointing that it's not easy to instruct it on how to fill in gaps so you can skip steps the same way you would in a human proof (which would only need a note saying that you're using associativity and parens are omitted thereafter, and any human reader will accept that as valid)

I originally intended to write what follows as its own comment but, although I used Coq instead of Lean and worked through a different set of exercises, your criticisms so closely mirrored mine, I decided to reply here instead, and point out promising paths to solutions.

I too felt it a waste of time to prove things that were clearly "obvious". Of course, in math, some of the most frightening words to encounter are "obvious" and "trivial" but in this case it really was trivial, at the level of proving `a + b = b + a` while working with integers. Tactics like auto, tauto, ring and field help here and should be given more and earlier emphasis in teaching materials. Tactics like `auto` perform like the proof search you mention and others like ring and field make cleverer use of structure.

To fill in the rest of the gap, a project like the Lean math library goes a long way. Not having to provide your own implementation of reals, differential forms or vectors over reals or complex numbers is incredibly useful. I was surprised by how difficult it was to find (I never did) a well maintained and documented library of basic common mathematical structures in Coq.

The second major issue is Formal proofs without their contexts (something like a debugger variables watch list in regular type code), are incomprehensible to most. However, a project, https://plv.csail.mit.edu/blog/alectryon.html, for Literate Formal proofs fully addressed that pain point for me. It's curious how the problem of tedium has a clear path to solution in the Lean community and the equally important flaw of write only proofs is being addressed within the Coq community.

Returning to the issue of what is obvious, a vast amount of mathematical knowledge is tacit, buried in the minds of the respective communities of pure mathematicians. For everyone else, especially users who cannot themselves provide proofs, mathematical knowledge is very often like a Potemkin village. Superficial and artifice, understanding that falls apart upon close inspection. This divide plays no small part in how difficult it is to properly learn mathematics outside of a mathematics department. Formalizing undergraduate math is important because it provides a solid foundation that leads to deeper understanding of mathematics when taken in aggregate across all participants. Even pure mathematicians have gaps once they step outside their field of expertise.

Actually there isn't much to understanding the tactics unless you want to use them similarly, just like you wouldn't bother looking into what "auto" has done. For understanding math it is a lot more important to understand the lemmas and why they are structured certain way, akin to understanding the API of programs. We can think of theorems as math's public API and lemmas the internal API for devs. In machine checked proofs lemmas often take on distinct flavors because how a human normally proves things may be hard to mechanize. Intead of tools for understanding tactics (granted, these could be useful for tacticians :) we really need tools to help us visualize structure of proofs. If I know how to write a lemma, tactical proof is rarely a blocking issue. Once it is checked the tactics become irrelevant. They were just there to convince the proof checker.

All what you say makes sense, especially as one becomes more comfortable with tactics but I maintain formal proofs are a lot harder to parse than regular math proofs. Having to write for both machine and human distorts a proof's natural flow and reading them often feels like trying to understand partially commented code by executing it in your head.

Well commented proofs are good to communicate intent but if you also want to be able to reproduce a similar proof, it's often useful to understand why tactics were deployed as they were. The existence of the wonderful https://plv.csail.mit.edu/blog/alectryon.html bears out the importance and utility of this.

> For understanding math

My contention, which I believe is shared by the article, is that this understanding is often flimsier than most think, particularly as one leaves well trafficked areas held together by tacit knowledge and knowledge of multiple reinforcing paths shared within communities with relevant expertise. However, even that is insufficient for less used lemmas.

This structuring of knowledge will be useful for mathematics education and research both, especially from the perspective of an individual human trying to safely use results of proofs.

> we really need tools to help us visualize structure of proofs

The output proof is a program, so the problem of visualizing proofs is much the same as visualizing programs and visual programming, sharing the same hurdles. Perhaps friendlier naming and formatting of output code in proof tools will be useful. I believe something more useful would be queryable visualizations of how theorems and lemmas connect and relate to each other.

The flimsiness of one's understanding tends to manifest as false "lemmas", which can't really be proved because one forgot certain conditions that are typically implicit with human understanding but must be made explicit formally. However if a proof can be completed then it's solid by definition. I would contend when a proof becomes hard to understand instead of documenting tactics one should break up the proof into more lemmas or create more subgoals; preferrably all tactics are "auto". It's nice that the tool you referred to is general and can be used to document any prospect of proof but being based on a markup language it is mostly static. When Gonthier mechanized Feit-Thompson Odd Order Theorem, he had very large graphs showing the relationship of the lemmas. Unfortunately those were also static as I remember and only really comprehensible to the experts. It would be nice to have interactive versions that can aid an average reader on comprehending and exploring the overall relationships. Such a tool is also sorely missing for understanding large code bases. The two are really two sides of the same coin through Curry-Howard. The good thing is a tool that lets users efficiently navigate structures can be done without extra effort of the proof writer (of course documenting intention is always important).

Outsider's question: is it likely that projects like Lean and Coq will ever feed into stuff that applied researchers find useful? By applied researchers I don't mean "applied mathematicians" but scientists who use maths in their field.

As an economist, I sometimes want to prove things that a real mathematician could do in their sleep. There's Mathematica and friends, but they have their limitations, i.e. they can do what you tell them but can't typically "find their own way" to the proof of a theorem. Might these systems ever come down to my level?

> but can't typically "find their own way" to the proof of a theorem

That's not what proof assistants like Lean and Coq are about. Sure, they can automate some trivial things, but generally their main utility is that they check your reasoning, not come up with it for you.

Yes, these systems are being used to formally verify implementations of cryptographic protocols, or implementations of numerical algorithms, for example.

Note that there are two distinct components that interact: (i) verification of proofs and (ii) automation of finding the proofs. The latter is very much an active field of research, but so far isn't of the level that it will prove most of your theorems for you.

Last month Kevin Buzzard gave an interesting talk "How do you convince mathematicians a theory prover is worth their time?" about how he became involved with LEAN and some of the proofs he formalised with it:

https://youtu.be/8PLrxAfmC_o

During Q&A there was a friendly quarrel about 'mainstream' vs 'constructive' maths. I think there's a funny analogy in here, if you let:

    mainstream proof : constructive proof :: program code : machine code

then Kevin is arguing that the idea of actually compiling his beautiful algorithms into machine code is silly, and that compiling program code in general is rather pointless.

I think that something like http://us.metamath.org/index.html has already gone a long way in formalizing math. And this is not the only attempt to formalize math, but it is unique that it uses a very limited amount of syntax and rules, and makes use of a simple (small) proof engine, which makes verifying that the proof engine is correct possible.

A small proof engine, and maybe a limited amount of rules (depending on the exact technical meaning of 'rules') is a good thing, but I'd say a limited amount of syntax is a bad thing. Mathematicians as a community tend to be happy with—I might even say to prefer—lots of syntax, and, if you want to get a formalisation process really going, layering it with enough syntactic sugar to bring in mathematicians who aren't usually 'formalisers' is going to be essential.

It's also true that there are lots of attempts at formalisation out there; I happen to know about vdash.org , for example, but there are certainly others. I think it's good to have an abundance of formalisations, since no one formalisation style is going to appeal to everyone (for example, as already discussed above, probably the more formalisation-minded mathematicians will have a higher tolerance for minimalism).

Lean allows for third party type checkers. There are relatively small alternative type checkers for Lean (e.g. a scala implementation [1]).

Lean's power lies in its elaborator that breaks down complex tactic-based proofs to a core proof language. This elaboration process can be extended with custom tactics and custom syntax, making it way more powerful than metamath.

[1] https://github.com/gebner/trepplein/tree/master/src/main/sca...

The problem with metamath is that you basically have to be a fully signed-up masochist in order to do anything nontrivial with it. People have certainly done nontrivial things with it e.g Carneiro and the prime number theorem -- but it takes all sorts. If I want to prove (a+b)(a+2b)(a+3b)= a^3 + 6ba^2 + 11b^2a + 6b^3 in Lean I just type `ring`. Good luck proving that from the axioms of a ring directly in metamath, I challenge you to do it in fewer than 30 moves. I should also say that whilst Metamath has certainly formalised a whole bunch of mathematics, it has not remotely gone "a long way" by any reasonable measure which a mathematician would use. For example, how much of an undergraduate mathematics curriculum does it have? How much representation theory? None. How much differential geometry? None. How much commutative algebra? Epsilon. These are the measures which mathematicians use, not lines of code. It is time that formalisation started to appeal to mathematicians, and for this to happen it is essential that it starts to demonstrate that it can actually do a lot of the kind of mathematics which is recognised as "completely standard undergraduate material and hence trivial" by mathematicians. It is still the case that these systems cannot do certain things which were known to Gauss or Euler (for example it was only this year that Lean learnt the proof that the class group of an imaginary quadratic field was finite, and as far as I know no other system at all has class groups -- but we teach this to the undergraduates!). Just saying "large code base therefore we've gone a long way" is not the correct logic. The question is how much of it is recognisable as worth teaching to undergraduates in 2021, and conversely how much stuff worth teaching to undergraduates in 2021 is _not_ in any of these systems. That's where the problems begin to show up. In Lean we are well into a project of formalising an entire undergraduate curriculum and within about two years we will have finished.

> The problem with metamath is that you basically have to be a fully signed-up masochist in order to do anything nontrivial with it. People have certainly done nontrivial things with it e.g Carneiro and the prime number theorem -- but it takes all sorts. If I want to prove (a+b)(a+2b)(a+3b)= a^3 + 6ba^2 + 11b^2a + 6b^3 in Lean I just type `ring`. Good luck proving that from the axioms of a ring directly in metamath, I challenge you to do it in fewer than 30 moves.

While it's allowed, generally Metamath users do not prove constructs directly from axioms, for exactly the same reason as you don't do it in Lean or traditional informal mathematics. You're right that most Metamath tools have fewer automated tactics, but there are tools with some automation, and people are working to improve that.

I absolutely love everything about this. Specially how it can provide access to knowledge to people all around the world.

I'm currently thinking about getting a degree in Maths, and I find extremely appealing the notion of having a repo of knowledge from where to gather theorems, specially useful for newer developed areas.

> However, AI works best with a database — and those databases are not yet there.

They do, but I would tell you that if that is your main motivation to create those databases, don't do it. The AI might spend milliseconds on work that takes man-years to compile, but get stuck on absolutely tiny issues of details it can't grok and which you can quickly explain.

If AI is the goal, I would propose to discuss with AI-researchers in the area of automated maths about what they can actually use to make progress. There are ways to have the AI learn unsupervised as much as possible, and to have it ask for supervision where needed.

In a similar way, it took a while to teach alphaGo to play go, but it only took a couple of extra years to have alphaZero play both go and chess without any database of example games.

I fully agree with the rest of the argument and I love the work that is being done to double check mathematics. But as AI researcher, I think this is a poor motivation and would warn against using it, as it might be very disappointing in the long run about how little of it turned out to be useful for AI.

If you read the article you can tell that AI is not the goal, it is a byproduct of the goal. The goal is to have confidence in the correctness of mathematical results proved by other experts.

Also, there has _already_ been some success on using AI to find proofs in lean.

There is a very active community around Lean ranging from mathematicians with no clue about computers to AI researchers trying to improve the automation. These AI researchers have explicitly said that bigger training sets will be very helpful. But like the sibling comment says, AI is not the main point.

The only major problem (IMO) is that Lean and the others (Coq, Hol, Isabelle, Agda, Idris, etc...) are all pretty hard to read.

Check out "Automated Propositional Sequent Proofs in Your Browser with Tau Prolog" for a promising approach: https://www.philipzucker.com/javascript-automated-proving/ It's rendering LaTeX proof trees.

Following this proof tree idea, this recent paper https://arxiv.org/abs/2102.03044 suggests to think of proofs of theorems as large trees, a tiny subset of which needs to be made explicit to convey the confidence the rest could be written out (if ever needed).

Does that presuppose that it's computationally expensive to verify proofs? If so, isn't that kind of unrealistic?

Verifying fully formalized proofs is cheap. What is expensive is to produce such formalized proofs. More precisely, to formalize a proof written in a typical math paper is extremely time-consuming and not so informative (that's why it's almost never done in practice).

Ah, cheers. :)

But doesn't that bring us full-circle to Buzzard's point? Isn't that why he's saying, "Hey gang, let's do math with machines." in the first place?

that is a neat demo with a lot of useful links! In fact, it seems that the Lean developers/community are very interested in new methods of achieving readability, and providing users with tools to build interfaces that scale up to the complexity of real workflows.

For example, Lean in vscode supports interactive html "widgets": https://youtu.be/8NUBQEZYuis?t=453

(at that timestamp, there's a quick introduction to their typical use at the moment).

lean4 is committed to all sorts of extensibility; here's a demonstration of the new macros: https://twitter.com/derKha/status/1354082976456441861. There have also been several instances of users implementing old lean3 features (for example, the `calc` tactic mode, which has unique syntax for proving (in)equalities) by simply defining new type classes and short macros.

Proof trees just become unmanageable for anything but trivial example and not only that, their biggest benefit - knowing which rule is applied, doesn't get you much for a dependent type system. Not to mention that any format that isn't just strictly text is probably doomed to fail from the start.

If you want essentially a text version of proof trees, just write fully annotated terms for your proofs. I think you'll quickly see that this just tends to make the proof _less_ readable because they become incredibly bloated.

Hmm... If not proof trees, what?

> Not to mention that any format that isn't just strictly text is probably doomed to fail from the start.

LaTeX is text. (I'm not being snarky.)

- - - -

The key might be in formalizing the subjective processes like what was described starting here:

> Mathematicians think in pictures

> I have a picture of the real numbers in my head. It’s a straight line. This picture provides a great intuition as to how the real numbers work. I also have a picture of what the graph of a differentiable function looks like. It’s a wobbly line with no kinks in. This is by no means a perfect picture, but it will do in many cases. ...

> If not proof trees, what?

Just make the proof language similar to the standard mathematics language and possibly process it with a presentation layer that makes it even better. The examples start from Mizar [1] (since 1973), IsarMathLib [2] (disclaimer: my project), Naproche-SAD [3] (bundled with Isabelle recently) [1] http://mizar.org/ [2] https://isarmathlib.org/ [3] http://ceur-ws.org/Vol-2634/FMM4.pdf

But the key difference between Mizar style proofs and Coq/Lean style proofs is just that the former is declarative and the latter is procedural. They're both ultimately just tactics based. Sure, a declarative style is nice when reasoning about equations, but otherwise the proofs simply degenerate into awkwardly written procedural tactics proofs.

> Hmm... If not proof trees, what?

I don't know. Both tactics and proof terms are already quite old (for CS concepts, that is) and there hasn't been any real competition, so I imagine in the medium-term we'll just see refinements of them.

>LaTeX is text. (I'm not being snarky.)

I can't imagine anyone wanting to read latex source code over tactics/proof term code. Unless you're talking about rendered latex? But that's not something people can realistically work with. Graphical proof assistants exist, but nobody uses them. For better or worse, plain text is simply king.

>The key might be in formalizing the subjective processes like what was described starting here:

In a sense, tactics are a very weak form of this. Instead of just describing a proof as its structured in the system, they allow a proof author to also describe some of their intent or intuition. It's definitely why some people prefer tactics based proofs. I imagine we'll see some attempts to incorporate some more of this into proof terms, but I don't know how successful this will be.

But honestly, I can't even imagine would formalizing something so subjective would even look beyond this. I'm not sure if it's even possible. If it is, I imagine it's going to be a radical departure from everything we know.

> Both tactics and proof terms are already quite old (for CS concepts, that is) and there hasn't been any real competition, so I imagine in the medium-term we'll just see refinements of them.

So it's really more of an issue of presentation? The techniques are fine? (I'm a professional programmer but an amateur logician, I really don't know what the big kids do.)

> I can't imagine anyone wanting to read latex source code over tactics/proof term code. Unless you're talking about rendered latex?

Yeah, you would generally only be looking at LaTeX source to debug your tools.

> But that's not something people can realistically work with.

I don't understand. I rarely work with it, but I was under the impression that it's pretty standard for writing math and science papers? Are there no WYSIWYG tools for working with rendered LaTeX? How do people work with it now, I guess is what I'm asking.

> Graphical proof assistants exist, but nobody uses them.

I just did a quick search and found two but they seem obscure:

https://en.wikipedia.org/wiki/Jape_(software)

https://github.com/liamoc/holbert

I guess the question I have is why does no one use them? Is it just inertia? I mean this is a thread about promoting the use of Lean et. al., so even the non-graphical, well-known tools are still kind of a niche, no?

Are graphical proof assistants only good for students and teaching, not "heavy lifting"?

In any event, I still feel that we can do better on the presentation side of things. (That's not controversial is it? The Lean folks are working on it?) I want to understand what kinds of software would help mathematicians.

> In a sense, tactics are a very weak form of this. Instead of just describing a proof as its structured in the system, they allow a proof author to also describe some of their intent or intuition. It's definitely why some people prefer tactics-based proofs.

That's pretty cool. :)

> I can't even imagine would formalizing something so subjective would even look beyond this. I'm not sure if it's even possible.

The Turing Machine is itself a formalization of a subjective process, eh?

If we get to the point where the machines can "read our minds" then it will be really easy. :) Heck, mathematicians can just watch videos of each other's mental imagery!

In the meantime, externalizing and formalizing these subjective intuitive processes with the machinery we've got seems like a fun and useful challenge, eh?

>So it's really more of an issue of presentation? The techniques are fine?

Well, both techniques are ultimately just a way of representing natural deduction (for a different proof calculus that isn't closely related to natural deduction you'll definitely need different techniques). Proof terms are the representation you get from the Curry-Howard Isomorphism (essentially the derivation is left implicit since it is unambiguous), while tactics based proofs are approximations of traditional proofs written in prose.

Are they 'fine'? Well, maybe there's some amazing graph-based way that will make current approaches look completely inadequate, but at the moment they work and we just don't know any better way.

>I don't understand. I rarely work with it, but I was under the impression that it's pretty standard for writing math and science papers? Are there no WYSIWYG tools for working with rendered LaTeX? How do people work with it now, I guess is what I'm asking.

It's definitely the standard, but I personally don't find working with diagrams in it pleasant (though I know some disagree). WSYIWYG tools exist, but don't find much usage. Everyone I know simply has a preview window open right next to their latex code, so it's not really an 'interactive' process. If you're fine with that, I'd just recommend generating latex code from proof objects/tactics scripts (which there already is some work on as far as I know). You should be able to generate e.g. proof trees very easily, they'll just be massive.

>I guess the question I have is why does no one use them? Is it just inertia? I mean this is a thread about promoting the use of Lean et. al., so even the non-graphical, well-known tools are still kind of a niche, no?

I imagine it's a combination of all sorts of factors. Proof assistants are very niche, the community is very academic and proof assistants require a lot of infrastructure which is why most users are concentrated among a handful of proof assistants. Proof assistants using dependent types (such as Lean) are also programming languages which I think naturally biases them towards text.

>Are graphical proof assistants only good for students and teaching, not "heavy lifting"?

I don't see any reason why that should fundamentally need to be - but I think the same applies to visual programming languages, which are essentially stuck in the same position for whatever reason.

>In any event, I still feel that we can do better on the presentation side of things. (That's not controversial is it? The Lean folks are working on it?) I want to understand what kinds of software would help mathematicians.

I don't think this is controversial at all - _how_ to improve presentation on the other hand might be.

>In the meantime, externalizing and formalizing these subjective intuitive processes with the machinery we've got seems like a fun and useful challenge, eh?

Sure, but anything beyond very incremental improvements also strike me as very hard, so it's not an area where I would expect much change for now, especially because there's still a good amount of low-hanging fruit in the area of proof assistants.

I will pay $3.14 to the first person that formalizes mathematics using only https://treenotation.org/.

This appears to just be saying “using python style indentation to represent trees”? I don’t understand the significance. Like, yeah, you can express whatever tree you want that way. Plenty of other ways to represent trees. It’s a nice enough default if you don’t know anything about the sort of thing the tree will contain.

But there’s a reason that when writing conditionals, we don’t put each symbol in the expression on their own line. Those also have their own tree structure, they are also part of the AST, but we put many of the nodes on the same line for ease of reading and editing.

> But there’s a reason that when writing conditionals, we don’t put one symbol in the expression on their own line

I won't disagree with you. However when you zoom out and crunch the numbers, you'll find that although there are infinite expressions to put in conditionals, in practice an absolutely minuscule amount of those patterns are actually used.

Context free grammars are not free.

Better ways are coming.

I wish these attempts were using constructive mathematics but I understand that that would turn away a lot of mathematicians.

Just pick a different one! There are definitely formalisation efforts out there that use constructive mathematics; for example Coq is so called after the logic, the calculus of constructions, that it uses (https://en.wikipedia.org/wiki/Calculus_of_constructions).

Hi! Yes! Just pick a different one! The problem is that constructivists have been formalising mathematics for decades and have not really managed to break through into the mainstream mathematical community with their efforts. The difference with Lean's maths library is that we absolutely reject constructivism, which makes Lean far less suitable for certain kinds of computations but conversely far far better equipped for proving all the theorems in an undergraduate mathematics curriculum and then going on to tackle research level mathematical questions of the kind which most mathematicians recognise as "normal mathematics". My argument (I should say that I am the author of the blog post) is that this resolutely non-classical approach is far more likely to arouse the interest of mainstream mathematicians, who rejected constructivism 100 years ago and have never looked back. I can certainly see a role for constructive mathematics, however I know from experience that most working mathematicians reject it and hence the pragmatic approach is to reject it when formalising if we are to start appealing to the mathematical masses.

The Four Colour Theorem in Coq seems pretty mainstream I'd say... Also I guess you know that you don't personally have to reject LEM to use Agda or whatever, you just can't do everything in it or at least everything the classical way.

This is a milestone result, and its formalisation taught us many things, for example that the systems are capable of handling long proofs about elementary objects.

However finite graph theory is not remotely mainstream mathematics. Take your favourite super-prestigious maths prize, for example the Abel Prize or the Fields Medal. Now look at everyone who has won this prize in the last 10 years. That is the definition of mainstream mathematics. And as you will see if you do this, the areas which these people are working on are a million miles away from finite graph theory. This is precisely the problem. Computer scientists sometimes have a very twisted view of exactly what kind of mathematics is regarded as important in 2021. The experiment I outline above will give you some idea of what is mainstream, and believe me, it's not the four colour theorem.

I suppose it's not exactly mainstream, but Kronheimer and Mrowka are among those trying to prove the four color theorem using instanton homology and gauge theory. It's certainly not finite graph theory, though (their idea of a 3-regular graph is the singular locus of a certain kind of orbifold!)

Finite graph theory is completely mainstream mathematics. There's a kind of elite provicialism that you sometimes see, where only the mathematics that's done at Harvard or wins the big prizes counts, and this is a good example. There are probably more people employed in math departments working on finite graph theory than there are working on the Langlands Program. Robertson and Seymour were too old to be eligible, but the fact that someone like them could never win the Fields Medal, while someone in other fields could, is a statement about who is well-connected with the prize committee, and not a general statement about mathematics.

And I say this as someone with no interest in graph theory, or combinatorics in general.

Buzzard's post suggests to me that when he says "mainstream," he means what the community at large thinks of as important and field-defining (cf. the sentence with important in it). He is totally correct here; in this sense finite graph theory is not mainstream mathematics.

Further, I don't think it is "elite provincialism" to point out this readily verifiable fact. Besides looking at the big prizes, we can look at any of the top journals (Annals, IHES, Inventiones, Journal of the AMS, Acta, whatever). You're not going to find a lot of finite graph theory there.

Now, I think we should separate the question whether it is the case that he's right about what mathematicians value from the question of whether it ought to be the case that the world is this way. As I just said, the answer to the first question is yes. I'd argue that the answer to the second question is also yes, but that's a whole different discussion.

Pointing to the top journals is again a statement about who is well-connected, so if anything it is further proof of my claim of elite provincialism. Mathematics has politics, like any other field, and it's politics that determine that the proof of the Robertson-Seymour Theorem appeared in the "Journal of Combinatorial Theory" and not JAMS.

The irony is that I suspect every single mathematician, elite or not, knows what the four-color theorem is, far more than could tell you what chromatic homotopy is, or state anything about the Langlands program beyond "Uh, it's something about number theory? And groups? Maybe?"

I think the (implicit) charge that the editors of top journals are keeping good papers out for snobbish reasons is mostly unfounded. I don't deny that their tastes shape what gets published, of course. But in most circumstances, they are not subject matter experts, and the first step of evaluating any paper is that is not an obvious desk-reject (for poor writing, crankery, etc.) is to send it to a group of relevant experts for "quick opinions." Only if these opinions are sufficiently positive is the paper sent for a full referee report (again by an expert), and in most (but not all) cases the referee's suggestion is followed. So the picture of editors just arbitrarily killing papers they don't like is not accurate.

Further, it's not like no finite combinatorics/graph theory gets published in these journals. Just not a lot, because it's not sufficiently interesting/valuable to the broader community. (Annals of Math almost published Hales's proof of the Kepler conjecture, after all; eventually a proof appeared in another top journal.)

Also, re: connections, you can easily check the author affiliations for papers in these journals. There are plenty of people from universities that are not so well known. It's hardly an "old boys club."

There was a notorious case that a paper by Wehring solving the largest outstanding question in lattice theory was rejected by JAMS despite glowing referee reports (and being pretty short). So it's pretty much an example of editors arbitrarily killing a paper. (It appeared in Advances in Mathematics.)

You can see a letter to the editor of the Bulletin about it. Look at the affiliations of the people protesting the decision, and the affiliations of the editors defending it: http://www.ams.org/notices/200706/tx070600694p.pdf

I don't really see a problem with this decision, though I am sympathetic to Wehrung. As the editors note, there are a ton of great papers JAMS doesn't publish (due to severe page count constraints at the journal). Their reasoning is not "arbitrary"; it was spelled out quite clearly for the authors in the rejection notice they got. Many other papers in "trendy" subjects face the same fate.

What do you think they say? "You're not well-connected, so we're rejecting you"? How do you think political decisions get defended in academia? For insiders, you listen to the referees. For outsiders, you invoke some vague criterion of lack of fit or lack of interest. And people can come along and say "If this field is important, why doesn't it appear in JAMS"? It's a self-fulfilling prophecy.

You seem determined to believe that the rejection was for "political" reasons despite having no evidence for this claim. The quoted reasoning was not "lack of fit" or "lack of interest," it was lack of "interaction with other areas of mathematics." Going back to my first comment, there's a general sense in the community that this sort of interaction among mathematical subfields (or with physics) is prized in research, and it's one of a few criteria that form the sociologically dominant view of what constitutes "good mathematics." You might disagree with these criteria, but it's not hard to see why that paper might lose out to other excellent papers when judged by them. This doesn't look like politics (favoring "insiders") to me; it looks like the consistent application of a value judgment about what good research is.

Again, whether you think the criteria should be the way they are is a separate conversation.

> resolutely non-classical approach

Calling this 'non-classical' is interesting—it's definitely non-classical from the point of view of formalisation, but I'm not sure formalisation has been around long enough to have classics ….

As of course you know but non-mathematicians may not, from a non-formalising mathematician's point of view, it's the non-constructive logic that's classical, to the extent that it's actually sometimes called classical logic (https://en.wikipedia.org/wiki/Classical_logic).

:-) Yes, by assuming classical logic the Lean community is taking a non-classical approach to bringing formalisation to the masses :-)

Dear Kevin,

I am working on some hobby projects, similar but very much more elementary to what you are doing. May I please kindly get your e-mail address (or you may drop me a note at ashok dot khanna at hotmail dot com). I would love to connect and follow your work.

I apologise as I was not able to find your e-mail address on your blog post - sorry if I missed it.

Best wishes,

AFAIK the advantage of constructivism is algorithms. Coq allows you to extract lisp/ML/Haskell programs. Perhaps we will be seeing the next generation of fully homomorphic encryption programs, or topological data analysis programs, automatically generated by Coq.

So what about an algorithm you verified in a non-constructive way?

You still need to construct the algorithm in the first place, which is what a constructive proof does.

Sure, but you would not need to prove it in a constructive way.

See, that is one of the problems with constructive mathematics. It not only requires you to write down the algorithm, but also to prove it constructively, although a non-constructive proof would be perfectly fine. In other words: constructivism is often overkill.

I think we're at cross-purposes; I am talking about mathematics for the purpose of real-life useful applications (e.g. cryptography, data analysis, etc), in which case you need algorithms.

Nope, we are not at cross-purposes. You just don't understand what I am saying.

Let's say you need an algorithm for a real-life situation, and you manage to write one down.

Ok then, you are good to go, just use it!

But ... how do you know that the algorithm you have written down is correct?

Now, a constructive mathematician would require you to also provide a constructive proof for your algorithm. A mainstream mathematician would additionally also be fine with a non-constructive proof for your algorithm. So, who is more real-life?

Yes, but if I told IBM that I had a proof that a particular algebraic property or relationship related to homomorphic encryption holds true, I'm sure they would much prefer that it was constructive, rather than non-constructive, because they can produce a usable algorithm from the constructive proof. The point is that by exploring mathematics using only constructive proofs, we are guaranteed to produce (possibly useful) algorithms. If you already have an algorithm, and can prove it works non-constructively then fine, but a collection of N non-constructive proofs is not nearly so useful for real-life applications as a collection of N constructive ones.

Your argument is wrong in so many ways, but let me just show you one: A constructive proof guarantees that there is an algorithm, but it doesn't say anything about the runtime of that extracted algorithm. Now, what good is an algorithm that is much too slow to be practically useful?

In general, my hypothesis is that if you restrict yourself to constructive mathematics, you are limiting yourself. And that is true whether your chosen field is algorithms, or not.

Now, if you offer me for a given algorithm a constructive proof, that's great. But if you needed 10 years to give me that proof, and a non-constructive one can be had in 10 minutes, I might not be so enthusiastic if I had to pay your salary, or if I needed that result really urgently, or both. But on the other hand, IBM probably doesn't care.

Hey, there's no need to by so impolite. My argument is not wrong, it's just a different argument to yours (which I fully understand, and is not difficult to grasp). Your example doesn't discount mine in any way; a slow algorithm is still better than no algorithm at all. The point about proving the correctness of an existing algorithm is moot, I'm talking about mathematical proofs which in themselve lead to algorithms. I'm not claiming we should abandon non-constructive mathematics, just that formalizing mathematics constructively leads to more useful algorithms. Similar to the argument that some programmers make about constraining themselves to think purely functionally in order to produce less buggy code. Goodnight.

Yeah, it's wrong. You could say that true and false are, just different. Well.

And you should have seen the answer that I wrote before that, and then deleted. Now THAT answer was impolite. Goodnight to you as well.

You probably have no experience with constructive proof checkers, else you wouldn't be missing Auggie's point.

> I'm sure they would much prefer that it was constructive, rather than non-constructive

One point against constructivism is that the proof could be less readable.

> can produce a usable algorithm from the constructive proof

No. Between the automated tactics and inductive propositions constructed to carry all kinds of redundant state helpful in proving your properties, your proof objects won't be anywhere near production level. And constructive proof checkers don't intend that to happen anyway: you pretty much define an efficient function in a DSL, then use a different DSL to prove that the function fulfils the properties. The proof object is pretty much a black box with unclear efficiency that wasn't meant for humans to read.

But everything you'd typically see in an algorithm has decidable equality, so proofs by contradiction are constructively justified, no?

I don't know! But I don't think so. Also think about other properties of an algorithm, like runtime, etc. You could have a non-constructive proof for the upper bound on the runtime, but not a constructive one.

Here is an example: after inputing positive integers a, b and c, output all natural numbers n for which a^n + b^n = c^n.

My algorithm: If a + b == c then output 1. If a^2 + b^2 == c^2 then output 2. Stop.

This algorithm is correct, because Fermat's last theorem holds. Now, try to come up with a simpler algorithm than that, and one that in addition has a constructive proof.

Fermat's last theorem holds constructively. This is because we can take the entire proof an rewrite it using the "classical fragment" of constructive logic[1]. I don't know if the proof of FLT (appears) to use the axiom of choice or not, but if it does we use Shoenfield's absoluteness theorem to remove any uses of the axiom of choice from the proof.

And we are done, because the statement of the theorem in the "classical fragment" of constructive logic is identical to the constructive statement as it does not involve any existentials or disjunctions. However if the theorem did involve a limited use of these connectives, we could use Goedel's Dialectica interpretation[3] to turn them in to their constructive counterparts, as long as the theorem is Pi_2 or lower, which is going to be the case for the vast majority of theorems about software.

[1] https://news.ycombinator.com/item?id=26217587

[2] https://en.wikipedia.org/wiki/Absoluteness#Shoenfield%27s_ab...

[3] https://www.andrew.cmu.edu/user/avigad/Papers/dialect.pdf

Hi Russell, thank you for clarifying this! So what you are saying is, if the algorithm and its correctness theorem have a certain form (which is usually the case), we can rewrite any non-constructive proof of it in a constructive way?

That is very cool! So, even less reason to demand a constructive proof, a non-constructive one is then often good enough even for hard-core constructivists.

Do you know if this has been implemented in any actual (interactive) theorem proving system, for example Lean? It sounds like a great feature to me to allow non-constructive proofs in certain situations, but to have the theorem hold even in a constructive setting.

Yes, I realize this arguments cuts both ways. One way is that you can write all these theorems in constructive logic, so there is no need for classical axioms. And the other way, is that users should freely use classical axioms because they can be mechanically removed.

Myself, I've never seen an automated theorem prover that will perform this sort of translation automatically. I have, on rare occasion, gone through by hand to remove uses of classical axioms in Coq proofs of theorems than ought not to be using them. Usually the uses are pretty superficial.

How difficult would it be to write a Coq plugin to perform these translations? The thing I like about Coq is that it appears to have better tooling than the other theorem provers (coqtop, proof-general for emacs), and you can extract code for other programming languages. I haven't looked in great detail at the alternatives though.

Isabelle also has code generation facilities and very good tooling, and uses classical logic.

Thankyou, I'll have a look.

I should mention that constructive mathematics, at least when done in dependent type theory, really starts to shine when things that normal mathematicians think of as propositions, are viewed as data. For example, normal mathematicians think of list membership as a predicate, but in dependent type theory, list membership is a value of an inductive family that is effectively an index of where that value occurs in that list (and in particular there could be multiple different values if that item occurs in the list at multiple different locations).

And dependent type theory is gleaming when things that normal mathematicians think of as propositions are not only values, but functions! For example a list l1 being a subset of a list l2 is a function from memberships of l1 (which, remember is data) to memberships of l2. Now you get partial evaluation when working on your proofs and things just magically unify.

I write about these examples in experience I had in "Taking Propositions as Types seriously" @ <http://r6.ca/blog/20171008T222703Z.html>.

There is a practical difference between Principia Mathematica taking 370 pages to prove 1 + 1 = 2 versus dependent type theory's proof `refl_equal 2`. (I'm exaggerating, but only a little).

Personally, dependent types never worked for me the way I thought they would when I first learnt about them (I was quite enthusiastic about them and about constructive mathematics initially). I found them too verbose, and too nitpicky. Your list membership is a great example: Usually, I am not concerned with where in the list does the element occur, list membership as a predicate is perfectly natural and usually adequate (but admittedly, if that's the only use case, better use a set than a list). I think an elegant mathematical argument wins not only by what is said, but also by what can be left unsaid.

But yes, being able to work with functions as data is also very important! That's why I am pursuing a combination of simple type theory and set theory as the foundation of a theorem prover, as I have outlined here: http://www.practal.com

Most are... like Coq, Agda, HoTT, etc.

AIUI, the Lean system does support constructive mathematics. You can add axioms and reasoning principles that make the system non-constructive, but they're entirely optional.

Yes, you are quite right, but the community around Lean's standard library heavily focuses on classical mathematics.

What is constructive mathematics for the layman?

Roughly, that proving a statement of the form "For all a,b,c,..., there exists x,y,z such that some statement involving a,b,c,...,x,y, and z is true." requires actually constructing suitable x,y, and z given suitable a,b,c, etc to derive them from.

Thanks

With the proviso that the non-constructive statement '∃ x such that P(x)' can also be understood constructively as '¬∀ x ¬P(x)' which does not require constructing a suitable x, so classical proofs can be modeled without adding any extra axioms to the logic. (Clearly the two statements are classically, though not constructively equivalent).

Similarly, all classical uses of LEM (A ∨ B) can be understood as constructive statements of the form ¬(¬A ∧ ¬B).

It's mathematics where certain kinds of proof by contradiction are not allowed -- if you want to prove that something exists because you want to use it, then you have to make it, you can't just say "let's assume it didn't exist and go on from there to deduce that 0 = 1 which is definitely wrong, so our assumption is wrong, so it exists, so let's use it".

Here is the reason why it's obvious for mathematicians. If you're trying to prove a theorem (e.g. the theorem that class numbers of imaginary quadratic fields tend to infinity), and then someone comes up with a proof which assumes that a certain generalisation of the Riemann hypothesis is true, and then someone else comes up with a proof which assumes that the exact same generalisation is false, then we mathematicians say "great, the theorem is now proved". This actually happened.

However if your boss asks you to write some code which does a calculation, and the next day you show up in their office with two USB sticks and say "this code is guaranteed to produce the correct answer if the Riemann hypothesis is true, and this other code is guaranteed to produce the correct answer if the Riemann hypothesis is false" then you are going to lose your job, because all you did was prove that the code exists, which is less helpful than it could be.

For me one of the biggest problems with the area of formalisation of mathematics is that for decades it has been dominated by computer scientists, whose view of what is important and beautiful in mathematics does not really coincide with that of the working mathematician. This is what I am fighting to change.

> This actually happened

Oh wow! Was it an interesting theorem that got proved this way? Did it get proved in another, less controversial manner as well? Could you provide a pointer to it?

https://en.wikipedia.org/wiki/Riemann_hypothesis#Excluded_mi... lists 3 such proofs.

I'd say it is still a pretty constructive answer, as you can run both codes, get two concrete answers, and one of them is guaranteed to be right.

A way to think about whether something is constructive is that everything is decidable, in the sense that there is some procedure that will give you the answer in finite time.

In Kevin's example where you have two programs, one which depends on the Riemann hypothesis being true and the other which depends on it being false, is that you can't just execute the programs -- they might have undefined behavior since they depend on the truth of some statement during their executions, and there's no general algorithm to decide whether undefined behavior is happening. They depend on undecided facts, so you can't put them together into a single program that decides the result. (Maybe a slogan is "truth can be contingent, but data cannot be.")

In Lean syntax, this is an example type signature of something that takes two programs (h and h') that respectively take in the truth/proof of a proposition or its negation, along with a proof that there is at most one element of α, and produces that element. I don't think there's a way to write this definition in Lean without marking the definition noncomputable:

  def extract {p : Prop} {α : Type*}
    (h : p → α) (h' : ¬p → α)
    (unique : ∀ (x y : α), x = y) : α := sorry

(the sorry indicates a missing definition).

Yeah, I really was joking.

“and one of them is guaranteed to be right.”

That’s where opinions will differ. That’s only true if you accept the law of the excluded middle.

Mainstream math does, but most constructive math does not.

Yup, I do accept the law of the excluded middle. Unreservedly. From a logical point of view, I cannot really imagine what it would mean NOT to be true.

Yes, Kripke semantics makes sense of constructive logic. Topos theory, too. But I really think of all of these embedded in classical logic, and assuming that the law of excluded middle doesn't hold for general reasoning just doesn't make any kind of sense to me.

Thanks Kevin. It seems like having both approaches is more flexible and thus more general (which can hopefully only be a good thing?). One could always replace a proof by contradiction later with a direct proof, but there's definitely value in using it in the meantime (at least in my uneducated view).

p.s. could you let me know your e-mail so I can keep for future reference, as I'm also working on a hobby project for automated theorem solving.

I remember when encountering my first (or one of my first) proof by contradiction (irrationality of sqrt(2), say) feeling unsatisfied because I didn't know how one could know that it was _your_ assumption that was wrong and not one of the more fundamental ones of mathematics.

There is only one kind of proof by contradiction. Assume not P, derive a contradiction which implies not not P, then conclude (via excluded middle) P.

If you assume P, derive a contradiction, then conclude not P, that is a direct proof of negation not a proof by contradiction.

Constructive mathematics rejects the law of excluded middle.

In a non-constructive mathematics it is true that 'either A or not A is true' and that allows you to prove existence of objects with certain properties by disproving their non-existence (if it cannot not-exist then it has to exist, by the law of excluded middle). Constructive mathematics, on the other hand, says that that's not enough and to prove that there exist objects with some properties you have to prove their existence.

Thanks

Constructive mathematics does not affirm excluded middle. That's distinct from rejecting it.

What do you mean? (sorry, english is not my first language).

The way I understand it is that if you have the law of excluded middle you cannot discard 'non-constructive' proofs as invalid since they follow straight from the axioms.

“Not affirm” means they don’t take it as an axiom (“we don’t take this to be obviously true”)

“reject” would mean that if, given their set of axioms, it could be proven, they would try and tweak their axioms in order to make it unprovable or provably false in their system (“we think this cannot and should not be true”)

So, “not reject” means they would happily use it in their proofs, if it could be proven from their set of axioms (“interesting. That gives us a powerful tool to do proofs”)

Constructive mathematicians do not assert that excluded middle is true since there is no constructive proof of (P not P). Nor do they assert that it is false, since that statement, (not (P or not P)), is constructively refutable i.e. there is a constructive proof of (not not (P or not P)). So there are no instances in constructive mathematics where excluded middle is false. But there are constructive settings where excluded middle holds, e.g. Boolean topoi, but you have to prove excluded middle is validated.

So we can't claim constructive mathematicians reject excluded middle, since they reject the rejection of excluded middle. I admit this will be confusing for people used to classical logic at first, even those for whom English is their native language.

> The way I understand it is that if you have the law of excluded middle you cannot discard 'non-constructive' proofs as invalid since they follow straight from the axioms.

This is accurate, my above point is just a pedantic one about semantics.

https://en.wikipedia.org/wiki/Intuitionistic_logic

If you are familiar with "Classical" logic, constructive math omits the law of excluded middle (e.g. "A or not A" must be true). In ZFC, the axiom of choice is omitted.

This leads to proofs that are not only a verification of some idea but also gives you the mechanism to compute the evidence. This is often described as "the computational content of proofs" and is especially valuable in the context of the Curry-Howard isomorphism: for every proof, there is a corresponding program (and vice-versa). This is the basis for formal verification of constructive proofs. When creating a proof in Coq, you are actually writing the corresponding program. And you can even extract the program in another general purpose programming language (usually OCaml in the context of Coq, but Haskell is also supported).

Many thanks

A lot of responses are going to say something like "it is mathematics without using the law of the excluded middle, or proof by contradiction" or something like that. They are not technically wrong, but I'd like to offer a different perspective.

The constructive logic used in constructive mathematics is classical logic with two new connectives added: the constructive existential, and the constructive disjunction (which could be defined in terms of the constructive existential).

The constructive disjunction and constructive existential connective has semantics given by the BKH interpretation[1]. A proof of the constructive disjunction A + B is either a proof of A or a proof of B. A proof of the constructive existential Σn:N. P(n) is a pair <n,p> where n is a natural number and p is a proof of P(n).

So constructive mathematics isn't classical mathematics hindered, but constructive mathematics is mathematics enhanced with a more expressive language. Naturally constructive mathematics tends to focus on theorems written in this more expressive language that make use of these new constructive connectives, rather than focusing on the classical fragment which is already well studied.

For the non-layman: we can see that the above interpretation is correct because the fundamental logical rules for universal quantification, implication, conjunction, false and true are all identical between classical and constructive logic. And, according to classical mathematicians at least, this set of logical combinatorics is complete. Thus the law of excluded middle holds, even in constructive logic, so long as you use the classical disjunction, which is defined in terms of conjunction, implication, and false. Similarly you can prove that proof by contraction, i.e. double negation elimination ¬ ¬A -> A is a theorem of constructive logic whenever A is a formula that does not use the constructive disjunction or constructive existential (where negation is defined in terms of implication and false).

For the all of the above, I'm particularly focused on first-order number theory, however all of the above carries over to higher-order theories, and I think it even holds for set theory (or at least some large part of set theory such as Zermelo set theory; I forget what happens with the replacement axiom). Higher-order constructive mathematics does come with the caveat that the Axiom of Choice is not a theorem of constructive mathematics even when it is phrased only using the classical existential.

[1]https://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%...

Thanks!

After working with Lean for a while, I've started to appreciate that there is a wider range of what it means to be constructive -- being "fully constructive" seems to me to be like fanatical efforts to make everything X, for example "everything is a function" or "everything is an object" and so on.

In the Lean approach, anything not marked `noncomputable` in the Type universe and above needs to be constructible, in the sense that there is a program that can compute such an object using a functional programming language (where the function is guaranteed to terminate), but proofs don't need to be constructible in the same way. Proofs are still functions, but they're free to use things like the axiom of choice in the course of a proof. The way things are set up, even if you use non-computable things while making your inferences, this "forbidden" data will not leak out.

It seems eminently reasonable to me that you can argue a program computes the correct thing because it doesn't compute the wrong thing, and unless you're specifically studying different toposes/logics, I'm not sure what constructive logic would really give you (and it's not like mathematicians slavishly keep track of where they used the axiom of choice or its consequence the LEM).

How this all looks in Lean practice is that it's stronger to give a definition and prove it satisfies a property than to prove a "there exists" statement. mathlib authors tend to go for the first, unless the result is inherently noncomputable. There's also a facility for lifting propositions up to boolean values, which more or less amounts to giving a constructive proof -- this is used pervasively, for example with finite sets, which are constructive in the sense that if you have one there's an actual finite list backing it.

I guess in short: it's a useful middle ground being able to prove something exists without having to construct it, but if you want to "have" the thing that purportedly exists you need to construct it.

There does not seem to be any reason for mathematicians to be turned about by these engines using constructive mathematics. One can use excluded middle as an axiom and do all the classical mathematics one likes. What becomes much easier if the engine is constructive is telling which theorems depend on excluded middle and which do not.

This is in fact how Lean works - the basic logic is constructive and excluded middle is an "extra" axiom. But even that is not as elegant as just writing non-constructive statements in the negative fragment of the logic, where (AIUI) one can already reason classically with no need for extra axioms.

I know we've discussed on HN before whether the elegance of the negative fragment extends to practice, but something about Lean is that it doesn't have LEM as an axiom. It's a theorem following from (a version of) the axiom of choice, the existence of quotient types, proof irrelevance (proofs of the same theorem are equal), and proposition extensionality (logically equivalent propositions are equal). Lean doesn't let you construct things that materially depend on LEM however -- you can only use it to prove that already constructed things have desired properties.

In case anyone is curious, the proof of LEM from AC is: Diaconescu's Theorem [0]

[0]: https://en.wikipedia.org/wiki/Diaconescu%27s_theorem#:~:text....

Reply on news.ycombinator.com