6 ms·

13M LoC, are we sure it didn't exploit any latent issues in the lean proof system?

tossandthrow 26d ago
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.
- Jaxan 26d ago
  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.)
  - tossandthrow 26d ago
    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.
- Jblx2 26d ago
  the Nanoda type-checker for Lean is ~5,000 lines of Rust: https://leodemoura.github.io/blog/2026-3-16-who-watches-the-provers/ 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.html 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 https://lawrencecpaulson.github.io/2026/07/30/Collatz.html
holmesworcester 26d ago
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!
Jaxan 26d ago
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.)
kingstnap 26d ago
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-the-kernel-soundness-bug-hunt/ 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.
- xvilka 25d ago
  Some argue that Lean breaks a few type-theoretical properties. See full discussion here: https://github.com/rocq-prover/rocq/issues/10871 https://github.com/rocq-prover/rocq/issues/10871
andriy_koval 26d ago
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.
- ajs1998 26d ago
  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.
  - andriy_koval 26d ago
    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.
    - drdeca 26d ago
      Within a given inference system, one can define concepts. This doesn’t add any axioms. It is, in essence, just a way to abbreviate things.
      - andriy_koval 26d ago
        ok, you now added some unknown inference system in addition to zfc
        drdeca 25d ago
        No, it is the same inference system. They are just abbreviations.
        andriy_koval 25d ago
Smaug123 26d ago
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.
- jmusall 26d ago
  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.
  - derkha 25d ago
    No, comparator does check the entire closure
  - Smaug123 25d ago
    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.
dist-epoch 26d ago
Anthropic surely is well aware. Most likely they asked separate agents multiple times to code review the proof and look for exploits.
jmusall 26d ago
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.
- qbit42 25d ago
  You just have to trust the statement and the lean compiler, not the proof. The compiler certainly still has remaining bugs, but I have never seen a bug leading to a false proof in good faith, only via obscure meta programming tricks. The nice thing is that the multiple versions of the compiler are constantly being stress tested. Still, there is plenty of work that could be done to make the compiler more trustworthy / easier to verify.
  - tsimionescu 25d ago
    This being 13M lines of entirely agent-generated code, we can't be certain it's written in good faith and doesn't actually exploit some weird metaprogramming trick. The agents' goal was to write a proof that Lean prints "correct" on, not to check that the proof of the FLT was valid (which they wouldn't be able to do anyway).
    - qbit42 24d ago
      It's not impossible, but I also know of no instances of an AI being told to prove something in Lean and exploiting such tricks. Surely Anthropic also had some agents looking for issues with the generated proofs. Personally, I am also comfortable trusting Kevin Buzzard, who was leading the human team aiming to formalize FLT and discussed this a bit on his blog. Finally, the good thing about Lean is that if anyone ever finds a new compiler bug (which, by the way, are being searched for extensively using AI), you can correct the bug and recompile any old proofs of which you are suspicious. Any tricks in a false proof must be exploiting a bug in the Lean compiler, so as we increase trust in the compiler over time we also increase trust in every previously compiled proof. I agree it's not a 100% guarantee, but in this case the human proof is well-understood and written about by many experts, so I think Claude had plenty of material to work with. Even if the task was enormous, I don't think any of the individual steps are out of the scope of what we have seen from current AI tools.

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.

Jaxan 26d ago
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.)
- tossandthrow 26d ago
  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.
Jblx2 26d ago
the Nanoda type-checker for Lean is ~5,000 lines of Rust: https://leodemoura.github.io/blog/2026-3-16-who-watches-the-provers/ 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.html 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 https://lawrencecpaulson.github.io/2026/07/30/Collatz.html

holmesworcester 26d ago

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!

Jaxan 26d ago

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.)

kingstnap 26d ago

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-the-kernel-soundness-bug-hunt/ 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.

xvilka 25d ago
Some argue that Lean breaks a few type-theoretical properties. See full discussion here: https://github.com/rocq-prover/rocq/issues/10871 https://github.com/rocq-prover/rocq/issues/10871

andriy_koval 26d ago

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.

ajs1998 26d ago
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.
- andriy_koval 26d ago
  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.
  - drdeca 26d ago
    Within a given inference system, one can define concepts. This doesn’t add any axioms. It is, in essence, just a way to abbreviate things.
    - andriy_koval 26d ago
      ok, you now added some unknown inference system in addition to zfc
      - drdeca 25d ago
        No, it is the same inference system. They are just abbreviations.
        andriy_koval 25d ago

Smaug123 26d ago

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.

jmusall 26d ago
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.
- derkha 25d ago
  No, comparator does check the entire closure
- Smaug123 25d ago
  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.

dist-epoch 26d ago

Anthropic surely is well aware. Most likely they asked separate agents multiple times to code review the proof and look for exploits.

jmusall 26d ago

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.

qbit42 25d ago
You just have to trust the statement and the lean compiler, not the proof. The compiler certainly still has remaining bugs, but I have never seen a bug leading to a false proof in good faith, only via obscure meta programming tricks. The nice thing is that the multiple versions of the compiler are constantly being stress tested. Still, there is plenty of work that could be done to make the compiler more trustworthy / easier to verify.
- tsimionescu 25d ago
  This being 13M lines of entirely agent-generated code, we can't be certain it's written in good faith and doesn't actually exploit some weird metaprogramming trick. The agents' goal was to write a proof that Lean prints "correct" on, not to check that the proof of the FLT was valid (which they wouldn't be able to do anyway).
  - qbit42 24d ago
    It's not impossible, but I also know of no instances of an AI being told to prove something in Lean and exploiting such tricks. Surely Anthropic also had some agents looking for issues with the generated proofs. Personally, I am also comfortable trusting Kevin Buzzard, who was leading the human team aiming to formalize FLT and discussed this a bit on his blog. Finally, the good thing about Lean is that if anyone ever finds a new compiler bug (which, by the way, are being searched for extensively using AI), you can correct the bug and recompile any old proofs of which you are suspicious. Any tricks in a false proof must be exploiting a bug in the Lean compiler, so as we increase trust in the compiler over time we also increase trust in every previously compiled proof. I agree it's not a 100% guarantee, but in this case the human proof is well-understood and written about by many experts, so I think Claude had plenty of material to work with. Even if the task was enormous, I don't think any of the individual steps are out of the scope of what we have seen from current AI tools.