What mathematicians should know about the Lean Theorem Prover

[u/al3arabcoreleone]

https://terrytao.wordpress.com/2026/10/09/what-mathematicians-should-know-about-the-lean-theorem-proverquestions-of-reliability-and-ai/

A brief explanation of proof assistants

[u/Nimmy_MTG]

I think there is an important point that Hales doesn't cover at all, which is what it means in practice to prove something in a proof assistant.

Specifically, the formalization of a proof in Lean almost never follows exactly the steps in the proof. However, unless it was done by a malicious adversary, the statement of the proof in Lean should not differ from what the paper claims to prove. (I won't comment on this here, but this is also worthy of discussion obviously)

The reason the formalization doesn't follow the steps is that some steps are hard to formalize. First, the computer is more rigorous than the average mathematician. For instance, any reasoning that states "without loss of generality" has to be done in a formalized proof in the full generality instead. Also some paper proofs use shortcuts that are familiar to any mathematician, but that you will have to explain very precisely to the computer. Last, you're building your proof from a mathematics library that is far from exhaustive: you cannot cite a paper in lean, you have to redo the proof of the result of the paper you cite itself if it's not already in the library. As a consequence, when you formalize a proof, you have to essentially redo all the lemmas, finding alternative paths that are easier to formalize because they rely on less literature, use less meta-arguments, and sometimes invent new lemmas and completely change the proof structure. Articles about formalization are interesting to read, because they provide actually a lot of insight about the original proof due to this.

Another reason of course the formalization doesn't always follow the steps is that you sometimes find mistakes in the proof. During his various talks on the proof of the Feit-Thompson theorem in Coq/Rocq, Georges Gonthier said that he did find a mistake in the original proof (I saw one of his talks back in the day, I don't know if some are available online). The mistake was easily fixed, but still a mistake.

Now all of this is about formalization of results obtained previously. When you supply a Lean proof at the same time as you supply a paper proof, the differences in how the proofs are done will still be there. Your Lean proof of some statement might be slightly convoluted to make it faster/easier to write, but you don't necessarily want this in your paper proof. However, at the very least, if you find a mistake during the Lean formalization, this should be reflected in your paper. This feedback loop has obviously been missing from many recent papers.

[u/djao → u/Nimmy_MTG]

Wait, what? "Without loss of generality" works just fine in a proof assistant. Both Lean and Rocq (via mathcomp) have a wlog command.

What is true is that you actually have to justify the without loss of generality claim fully. But making the claim itself is supported.

[u/Standard_Jello4168 → u/djao]

I think that was just an example, wlog exists but as you said you have to prove that the statement is symmetric which can be "obvious" but still rather annoying, and since lean is much more rigorous a slightly different proof that is worse in writing may be an easier version to code.