Who we trust when we trust Lean
Ken Thompson famously wrote “Reflections on Trusting Trust”. He asked, “To what extent should one trust a statement that a program is free of Trojan horses?” He imagines malicious code that finds its way into compilers and hides its own presence. His conclusion is, “You can’t trust code that you did not totally create yourself… No amount of source-level verification or scrutiny will protect you from using untrusted code.”
Today, in the age of AI, which increasingly has the capability to deceive us and to exploit software vulnerabilities, we absolutely cannot put blind trust in systems such as Lean.
This is the cybersecurity parallel to formalized proofs. Reflections on Trusting Trust (Thompson 1984) affects how compilers are developed. The Rust compiler, for example, is built by default by downloading a recent beta rustc, so you are trusting a binary you didn’t create. The way out is to bootstrap from something small enough that a human can audit it fully: mrustc, a Rust compiler written in C++ whose primary goal is bootstrapping rustc, is how Guix built Rust from source, and Guix’s whole package graph is now rooted in a 357-byte program.
Lean’s kernel is like that. Hales again:
The Lean kernel is several thousand lines of C++ code. […] Lean proofs should never be believed until they have been checked by the kernel. Additionally, a proof in Lean should not be accepted until a human audit is performed to ensure statement fidelity. Is the verified theorem what we think it is? Do the definitions in Lean correspond to what we think they should be? This task is generally massively easier than checking the proof itself.
And the counterpart of building rustc with mrustc is checking a proof with another kernel. “About 25 kernels for Lean have been written”, and the Navier–Stokes formalization “has already been confirmed by more than a dozen proof-checkers”.
This is the picture I drew in my talk on agentic engineering in math and RSE:
An AI proof in Lean is like the left: very watertight. Green means you don’t need to check it. Any opening is where you need to inspect: the translation of the statement,
sorry, axioms, and so on.
One useful mental model, not exact logically, is to ask the probability that a proof is wrong, \(P(\text{wrong} \mid \text{how it was proved})\). By a human:
- “Just” a proof, in natural language: like how it has been done for ages, and continues to be done in most papers.
- A formal proof, in Hilbert’s sense, where every step is an axiom or follows from earlier ones by a rule of logic, but checked by hand.
- A formal proof written in Lean.
By an LLM/AI:
- A proof in natural language.
- A formal proof written in Lean.
If I have to order them by that probability, where \(\ll\) means orders of magnitude apart:
\[ \begin{aligned} P(\text{wrong} \mid \text{Lean, human}) &\approx P(\text{wrong} \mid \text{Lean, AI}) \\ &\ll P(\text{wrong} \mid \text{formal by hand, human}) \\ &\ll P(\text{wrong} \mid \text{natural language, human}) \\ &< P(\text{wrong} \mid \text{natural language, AI}) \end{aligned} \]
The two Lean proofs are about the same, as the kernel doesn’t care who wrote the proof, as long as a human has checked the openings of the picture above, the translation of the statement especially. The key difference between them is understanding and reusability. A formal proof by hand has no gaps, but it is so long that the human checking it becomes the weak link, which is why, as Hales says, it is generally done by computer.
There is a second translation though, of the proof, and that is what Bastounis et al. (2026) go after:
The purpose of this article is to demonstrate why this process may offer no confidence in the original NL argument, owing to the various difficulties in performing the translation semantically faithfully. […] In particular, we show that the formalised Lean proof does not correspond to the NL proof of blow-up of solutions to the Navier-Stokes equations.
When an AI translates its natural-language proof into Lean, the kernel only checks that the Lean proof proves the Lean statement. Along the way the AI may “repair” the proof:
A revision may repair an error or replace a correct argument by another one […]. Both count as success under this criterion, and neither establishes fidelity to the original purported proof. In fact, since the above procedure accepts any valid Lean proof, if the original NL proof is indeed incorrect, the AI is incentivised to find a different proof.
So the Lean proof can be correct while the natural-language proof, the paper written for humans to read, is wrong. In the Navier–Stokes case, the Lean code “often has stronger conditions on bounds on the derivatives of various functions than the corresponding results in the NL paper”, though the authors make no claim about whether the paper itself is correct. In terms of the ordering above, the Lean proof is \(P(\text{wrong} \mid \text{Lean, AI})\), but the paper is still \(P(\text{wrong} \mid \text{natural language, AI})\).
Both the arXiv paper and Hales are pointing out that the chain can’t be trusted 100%. But that is not a contradiction of this ordering: the probability that something proved formally is wrong is still much closer to 0 than otherwise. Hence the formalization in Lean is a huge boost in confidence, and that’s what gives an LLM a verifiable signal. For a human, it is often the bare minimum to be convinced there’s something here worth investigating. So while it is important to calibrate our mental probabilities given a Lean proof, I can’t stress enough the value of a Lean proof in AI math: without it, we wouldn’t even start to debate its values and harms.
One way I see it is that thinking in probabilities like this shows the difference between a mathematical proof and a scientific one. Not even a mathematician can be totally certain, as humans and machines can err, so the primary difference is what they aspire to obtain. A scientific statement aspires to a small \(P(\text{wrong})\). For a discovery in particle physics, for example, 5σ is the gold standard: about a one in 3.5 million chance of making that observation if the current theory’s prediction were right. A mathematical proof aspires to \(P(\text{wrong}) = 0\), a boolean True. The 25 kernels are the scientific way of getting closer to it: every independent check makes \(P(\text{wrong})\) smaller, so the more the merrier.
So Hales is not wrong, but I think he is telling the story wrong. Yes, there’s always a chance the proof is wrong, which is why I put those probabilities above. But to say some of those LLM Lean proofs might be wrong, or even worse, that they might be exploiting kernel bugs to prove them right, is very hypothetical. As far as I know, there are no known cases where this happened, once a human has verified that the statement means what we mean and checked the axioms it uses. The summer’s soundness bugs were found by people who went looking for them.1
The real practical issue then is not whether the probability is close to 0, but who you’re really trusting. And I think that is the point of the original Trusting Trust too. Its abstract asks the question Hales quotes, and answers it this way:
To what extent should one trust a statement that a program is free of Trojan horses? Perhaps it is more important to trust the people who wrote the software.
No one totally creates everything themselves, so you always need to trust someone, kind of in the web of trust sense. Trust, in this sense, is in what you can’t completely verify: verified means no trust needed. One implication is that when an LLM is in the chain we should be more skeptical, because it is not part of our web of trust. But more importantly, we should point out that the trust we’re putting in a Lean proof is in the designers of the kernel, Leo de Moura and the Lean FRO, and as an extension, all the 700 and more people authoring mathlib. Without these people in the inner circle none of this can happen. So they should be credited, and we should continue to fund them to improve this critical area that we are putting all our trust in.
References
Footnotes
The kernel exploits I know of all came from people looking for bugs. In the summer’s bug hunt, an internal OpenAI model found kernel bugs and exploited every one of them to get the kernel to accept a proof of
False(de Moura 2026b). Ramana Kumar’s AI-assisted “disproof” of the Collatz conjecture exploited a bug in the kernel’s handling of nested inductive types, and the independent checker nanoda had a bug of its own that let it through too (de Moura 2026a). The closest to a counterexample is reward hacking on benchmarks: some DeepSeek-Prover-V2-7B proofs on miniF2F and PutnamBench passed the benchmarks’ checks while depending onsorry, through a bug in theapply?tactic before Lean 4.20 (Ammanamanchi et al. 2026; Bodla Krishna Vamshi and Yang 2026). The kernel was not fooled there, and checking the axioms the proof uses catches it.↩︎