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

70

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.

19

u/satanic_satanist 3d ago

Once should know about that kernel bug that it didn't occur through normal Lean usage but using metaprogramming to circumvent the checks that usually run before anything reaches the kernel. It's not like that Collatz proof looked anything like a normal proof to someone who has taken half a day to get acquainted with Lean's syntax

1

u/flabbergasted1 3d ago

Thanks for the clarification - could you explain a little more what this means? As in they used software to generate a non-standard "malicious" proof that is evaluated differently than a normal proof(?)

I'm curious how this works and what it does or doesn't tell us about Lean and the formalized results in mathlib.

7

u/tricky_monster 3d ago

They used meta-programing to implement a special proof that can't really be written using the "user facing" syntax.

Like if you wrote a program in binary directly instead of using the C compiler I guess (using macros if we really want to extend the metaphor).