What a Lean proof really guarantees behind AI breakthroughs – and what it doesn't

What this is about

In just over two weeks, five major AI announcements have pointed to the same seal of approval: “machine-checked in Lean.” Anthropic had 1,000 Claude agents formalize Fermat's Last Theorem. Google DeepMind says it has proven security guarantees for the Signal protocol. OpenAI and Anthropic independently report a refutation of the Exponential Time Hypothesis (ETH). The company Physical Superintelligence (PSI) presents a proof of the Aaronson-Ambainis conjecture. And Google DeepMind and Google Quantum AI unveil quantum programs that, according to their paper, need up to 290 times fewer resources.

Lean is a programming language for proofs. A small core program, the kernel, checks every logical step. That's a strong guarantee, but it has precise limits. This article shows where those limits are and gives you four questions to test any claim.

What the kernel actually checks

The kernel answers exactly one question: does this statement follow from the permitted basic assumptions via this proof? There are three things it doesn't check.

First, what the statement means. Lean compares the proof with the statement that was typed in, not with the headline. Thomas Hales makes this point in a detailed guest post on Terence Tao's blog on October 9: a human has to confirm that the formal statement matches the intended one. That includes basic notions such as real numbers, derivatives or measures. But that is “in general massively easier than checking the proof itself,” he writes.

Second, whether the kernel itself is bug-free. Hales calls July and August 2026 a “summer of soundness bugs.” Soundness bugs are bugs that make Lean accept something false as proven. One of them enabled an illegitimate “disproof” of the Collatz conjecture, and a related one a bogus proof of the Kepler conjecture. All of the bugs were fixed, and Mathlib, the Lean community's large mathematics library, was re-checked with the repaired kernel. According to a LessWrong post by Milo Moses, a joint search by the Lean FRO, the organization behind Lean, and OpenAI subsequently turned up six more bugs. Hales therefore recommends cross-checking proofs with several independently written kernels.

Third, which assumptions went in. These include axioms, principles accepted without proof. Three are standard (propext, Classical.choice, Quot.sound), and Mathlib builds on them too. Things get critical with additionally introduced axioms, with shortcuts like native_decide (which accepts the result of a compiled program without checking it) and with sorry. sorry is a placeholder that marks a gap as “proven.” The Lean FRO's comparator tool checks much of this automatically. It ensures that the proven statement matches a challenge file fixed in advance, that no disallowed axioms appear, and that everything goes through the kernel. But according to its documentation, what a self-defined concept means still has to be checked by a reviewer, “possibly a human.”

The biggest gap: misformalized statements

A case from January 2026 shows how this goes wrong in practice. A publicly available Lean formulation of the Navier-Stokes problem was flawed. On the Lean Zulip, the community's discussion forum, Mirek Olšák showed that the combined statement was a tautology, meaning it followed from logic alone. He wrote a compiling “solution” that exploited exactly those flaws.

Research confirms the pattern. In the MechGeo paper (arXiv 2608.02295) on geometry problems in Lean, 16 automatically generated statements turned out to be disprovable and had to be fixed by experts. In “Sorries Are Not the Hard Part” (arXiv 2606.13925), Vasily Ilin and Brian Nugent describe an AI formalization that compiled without a single sorry. Even so, reviewers found serious problems with definitions and generality. Their standard: a formalization is only good once it survives expert review. That's why the FormalProofBench benchmark (arXiv 2603.26996) had humans check its 200 problems for misformalization a second time. The paper doesn't say how many errors turned up.

The model, not reality

Even a correctly formalized statement is often about a model rather than the world. A proof about a model of computation, a simulated processor or a cost measure only holds as far as the model matches reality. That's exactly where several of the current announcements stop.

The checklist: four questions for every “AI proves X” story

1. Which statement, exactly? Is there a short, readable Lean statement, and has an independent human compared it with the original?
2. Which assumptions? Only the standard axioms, no sorry, no native_decide? And are extra assumptions hidden in the statement itself, say as “if X holds, then …”?
3. What is the proof about? The real object (theorem, binary code, runtime) or a model of it, and how far is that from the headline?
4. Who checked it outside the lab? Are the files public, is there a second kernel, and have independent experts weighed in?

The five cases, checked

Fermat. This is the model case. According to the repository's README, the final statement says, in essence: for n ≥ 3 and positive a, b, c, aⁿ + bⁿ ≠ cⁿ. It uses only Lean's built-in natural numbers. The build fails if anything other than the three standard axioms shows up. Comparator confirmed the match with the challenge file, and the independent kernel nanoda checked 1,052,234 declarations without errors. The README names the remaining gap itself: no tool checks whether every intermediate lemma means what its name promises. For the final theorem that doesn't matter, but it does for reusing the building blocks. 106 files come from Kevin Buzzard's human FLT project and from flt-regular. Buzzard praises the achievement but, according to The Next Web, calls it mathematically meaningless: it “faithfully follows the early literature and adds nothing.” For the new 1,000-agent run, the summary available to us mentions only the kernel check. Who wrote the 60 target statements remains unclear.

Signal. This one deserves a close look, because DeepMind went further than usual. Until now, Signal has mainly been verified at the level of protocol models, for example with the tools ProVerif and CryptoVerif for PQXDH and SPQR. The community project Signal Shot, by contrast, aims to translate the Rust code into Lean using the Aeneas tool. According to its project page, DeepMind verified the compiled machine code of libsignal 0.105.4 and spqr 1.6.0, running on a Lean model of an ARM processor (AArch64 on Linux, 467 instructions, 31 system calls). That adds up to around 6.5 million lines of Lean. sorry and native_decide are rejected.

You still have to trust quite a bit: the processor model, which was tested against emulators, and contracts for 37 routines such as X25519, Kyber1024 and AES. On top of that comes a symbolic security analysis in which hashes “never collide.” Only conversations between two people are covered, not group chats. Side channels, meaning attacks via power consumption or timing, are left out. The computational security guarantee doesn't hold against quantum attackers and becomes worthless in very long sessions, from roughly 25,000 messages according to the paper. That's not a flaw but an honest description of the scope. It just doesn't support the headline “Signal proven secure.”

ETH. Anthropic's README is unusually candid here. Lean checks the proofs, “but no machine checks that this file says what the paper says.” The statements refer to a specific Turing machine variant from Mathlib, a mathematical model of a computer. According to commentator Carlos Toledo, OpenAI's Lean code doesn't define the ETH itself at all. Between November 4 and 5, volunteers in a GitHub issue built a bridge proof to a standard multi-tape Turing machine. But they too write that the equivalence of the definitions was “read, not decided.” What's more, the statements, the bridge and the checking script come from the same person, and the proofs were written by Claude. The organizers Impagliazzo, Paturi and Williams hadn't published a verdict as of November 8. In practical terms: according to a calculation cited by toknow.ai, OpenAI's guaranteed bound only beats brute-force search for formulas with around 2^1,000,000,000 variables.

Aaronson-Ambainis. The evidence here is now much stronger than in our first report. The repository names the Lean statement PrintedConjecture, uses only standard axioms and no sorry, and was additionally checked with lean4lean. A fourth, sharper theorem is conditional, though: it relies on an external result that hasn't been formalized. According to the README, a human reader should confirm whether PrintedConjecture matches the 2008 conjecture. A Stanford group led by Guy Blanc is reading the proof, and Scott Aaronson writes on his blog that he believes it's correct. He gives two reasons: the Lean certificate and the expert review. But he admits he hasn't understood it himself yet.

Quantum programs. In the paper (arXiv 2611.09822), humans write the specification in Lean. Programs and proofs start out marked as sorry, and the agents fill in these gaps. A checker then uses Comparator to make sure target theorems, definitions and permitted axioms stay unchanged. Still, the result isn't foolproof: the authors report that agents found a loophole in the specification, namely the way Toffoli gates were counted. It could be exploited without improving the circuit, and the specification had to be revised.

Above all, the proof doesn't measure speed on real hardware. The cost measure is the number of logical qubits (error-corrected computational bits) times the number of T gates, a particularly expensive operation:

The 290-fold saving was achieved partly with classical simulation. Error-correcting codes, qubit routing and chip layout are explicitly left for future work. According to the authors, even after the improvements, the programs still need “far more resources” than the first fault-tolerant quantum computers will offer. The code is supposed to be released “soon.” Until then, question 4 can't be answered.

Our take

Our assessment: “machine-checked” isn't an empty marketing term. In all five cases, an error in the proof chain itself is unlikely, provided the kernel is correct. The labs have learned: Comparator, second kernels and open repositories are almost standard now. But the guarantee only covers the statement that's actually written in Lean. And depending on the case, that's either one line about natural numbers or 26,000 lines of specification plus a processor model.

The further the Lean statement is from the headline, the more depends on humans comparing the statement with the original. That work isn't finished for ETH, and for the quantum programs outsiders can't even do it yet. For you as a reader, that means: don't ask “Was it checked by Lean?” Ask “What exactly was checked, and who read the statement?” If a story says nothing about that, that's already your answer.