This is a crucial point. There have been many bugs in Lean (and in other proof assistants for that matter). Proof assistants work well on human input, because it was created with a certain intent.
We simply don’t know what those 13M contain and whether it “makes sense” and doesn’t trigger Lean bugs. (There are “independent” lean verifiers, but historically they contained the same, or similar, bugs.)
It is possible, although the post notes that the proof was also verified by the Comparator, which means any exploited bug has to also be present in that checker. Which is not unheard of, but is much less likely than merely an exploit in Lean 4.
The comparator was only used to verify that the final statement indeed is a valid formalization of Fermat's Last Theorem, not that the proof leading up to it is correct.
I think this isn’t true? Comparator verifies proofs; it’s not clear to me what it even means to mechanically verify a statement to be valid. The statement is manifestly valid anyway - it’s hard to find much simpler statements of maths, slightly odd facts of mathlib’s natural arithmetic like the saturating behaviour of natural subtraction notwithstanding.
That must have slipped through Kevin Buzzard's review, which is not entirely unplausible with 29500 theorems to verify...
I think they should spend another few billion tokens and let agents try to disprove any of those statements or links between them. Then I'd be a lot more convinced.
Not just lean, but math foundation itself, I am not strong expert, but my understanding is that there is no fully recognized axiomatic foundation for modern math, all proposals could lead to some weird results.
There is, or rather are, fully recognized axiomatic foundations. You are free to choose one you like. Of the most popular ones is ZFC or ZF, but there are others (some lead to the same results some not). The main criteria for popularity is how useful it is. You can even make your own axiomatic where 2+2=5, but it would be useless.
You probably heard about Goedel Incompleteness -- the proof that the the axiomatic itself cannot be proven, like using ZFC to prove ZFC, but that's another topic.
It would be fun to play with this Anthropic/Lean formalization under different axiomatics.
ZFC is probably the biggest foundation, and only Choice is apparently controversial. The results aren't that weird, they're just different and occasionally more useful than using !Choice.
do we know if claude's formalization is built on top of zfc and not zfc+extra?
zfc itself is not sufficient, you need some layers of extra concepts formalization to fit specific problem domain(e.g. zfc doesn't define even basic arithmetics), which also could have potential issues.
Most systems i have seen are way beyond a 100 lines. And their GitHub repository contain many issues, often soundness bugs. (Granted, many get fixed very fast.)
The AI labs have out considerable effort in trying to find and patch lean exploits. They explicitly set agents and have them try to prove false.
> Daniel used OpenAI internal models to discover new soundness issues in the official Lean kernel and runtime
https://leodemoura.github.io/blog/2026-8-24-postmortem-for-t...
They found several bugs and they have patched them. Lots of work going into making sure lean is sound.
This is a crucial point. There have been many bugs in Lean (and in other proof assistants for that matter). Proof assistants work well on human input, because it was created with a certain intent.
We simply don’t know what those 13M contain and whether it “makes sense” and doesn’t trigger Lean bugs. (There are “independent” lean verifiers, but historically they contained the same, or similar, bugs.)
It is possible, although the post notes that the proof was also verified by the Comparator, which means any exploited bug has to also be present in that checker. Which is not unheard of, but is much less likely than merely an exploit in Lean 4.
The comparator was only used to verify that the final statement indeed is a valid formalization of Fermat's Last Theorem, not that the proof leading up to it is correct.
I think this isn’t true? Comparator verifies proofs; it’s not clear to me what it even means to mechanically verify a statement to be valid. The statement is manifestly valid anyway - it’s hard to find much simpler statements of maths, slightly odd facts of mathlib’s natural arithmetic like the saturating behaviour of natural subtraction notwithstanding.
No, comparator does check the entire closure
That must have slipped through Kevin Buzzard's review, which is not entirely unplausible with 29500 theorems to verify...
I think they should spend another few billion tokens and let agents try to disprove any of those statements or links between them. Then I'd be a lot more convinced.
Nope! :(
Meaning, people and LLMs are finding 1=0 bugs in formal verification tools. I have no idea how likely this is in this case, though!
Anthropic surely is well aware. Most likely they asked separate agents multiple times to code review the proof and look for exploits.
Not just lean, but math foundation itself, I am not strong expert, but my understanding is that there is no fully recognized axiomatic foundation for modern math, all proposals could lead to some weird results.
There is, or rather are, fully recognized axiomatic foundations. You are free to choose one you like. Of the most popular ones is ZFC or ZF, but there are others (some lead to the same results some not). The main criteria for popularity is how useful it is. You can even make your own axiomatic where 2+2=5, but it would be useless.
You probably heard about Goedel Incompleteness -- the proof that the the axiomatic itself cannot be proven, like using ZFC to prove ZFC, but that's another topic.
It would be fun to play with this Anthropic/Lean formalization under different axiomatics.
Interestingly, in his ICM 2026 lecture, Terence Tao specifically mentioned that Lean is not based on ZFC.
> Goedel Incompleteness -- the proof that the the axiomatic itself cannot be proven, like using ZFC to prove ZFC, but that's another topic.
Godel theorems are for systems with basic arithmetic, zfc doesn't include arithmetic, thus are not object of Godel theorems.
22 replies →
Lean is based on Type Theory not ZFC.
ZFC is probably the biggest foundation, and only Choice is apparently controversial. The results aren't that weird, they're just different and occasionally more useful than using !Choice.
Reply to sibling - lean4 doesn't rest on ZF or ZFC. https://lean-lang.org/theorem_proving_in_lean4/Axioms-and-Co... However I believe an equivalence of power has been shown between the two.
1 reply →
do we know if claude's formalization is built on top of zfc and not zfc+extra?
zfc itself is not sufficient, you need some layers of extra concepts formalization to fit specific problem domain(e.g. zfc doesn't define even basic arithmetics), which also could have potential issues.
3 replies →
The proof system is relatively easy to verify.
I am not entirely sure about lean, but the core algebras for systems like lean are in the 100s of lines of code.
You can likely convince yourself it is correct in a weekend or less - especially with an Ai to help you understand it.
Most systems i have seen are way beyond a 100 lines. And their GitHub repository contain many issues, often soundness bugs. (Granted, many get fixed very fast.)
You need to understand the concept of the core algebra and 100s (with the s), then I think you'd be better positioned to understand my comment.
And granted, I don't know the exact details about Lean. It might be that they don't have an incredibly simple core - as has elsewise been the norm.
the Nanoda type-checker for Lean is ~5,000 lines of Rust:
https://leodemoura.github.io/blog/2026-3-16-who-watches-the-...
...and for those who are looking to roll-their-own:
https://ammkrn.github.io/type_checking_in_lean4/title_page.h...
...and some thoughts on putting stuff in the kernel:
https://lawrencecpaulson.github.io/2026/07/30/Collatz.html