r/math • u/al3arabcoreleone • 4d ago

What mathematicians should know about the Lean Theorem Prover

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

364 Upvotes

97% Upvoted

33 comments sorted by

View all comments

68

u/flabbergasted1 3d ago

Really fantastic read, thank you for sharing. I didn't know any of the details on Lean proofs & checkers.

I was surprised to hear about the kernel "soundness bugs", which is jargon for: the program entrusted to run/verify Lean proofs verified a proof of "False".

One Lean bug led to an illicit disproof of the Collatz conjecture. I learned of the bug this summer when it produced a short illicit proof of the Kepler conjecture in Lean.

This feels like a huge deal, though it sounds like those close to the situation feel that -- since these "bugs" were found with the help of a concerted AI search for them -- it's comparatively unlikely any bugs survived.

Still, my (very informal) gut takeaway is that Lean formalization is an advance in proof-checking but certainly not infallible as a system. It's harder to pass off a bogus proof than it was when (say) Kempe's faulty proof of the Four Color Theorem was accepted as valid from 1879-90. But it's a difference in degree, not kind: the types of errors or "bugs" are further up in the hierarchy of abstraction and more easily identified.

108

u/flabbergasted1 3d ago

Also found this funny:

We would like to possess a formal proof that the Lean 4 kernel has no bugs. However, Gödel’s second incompleteness theorem places severe limitations on this undertaking.

Obvious, I suppose, but still funny that Gödel poses a technological limit on a debugging program. Weird timeline.

51

u/BijectiveForever Logic 3d ago

Maybe I am too close to this (being a computability theorist), but since the halting problem is in some sense Incompleteness With A Hat On, this doesn’t seem weird to me at all!

22

u/TashanValiant 3d ago

Incompleteness with a hat on might be the best phrase I’ve heard for the Halting Problem