Who we trust when we trust Lean A 2026 analysis by Bastounis et al. finds that a formalized Lean proof of blow-up of solutions to the Navier-Stokes equations does not correspond to the original natural-language proof, arguing that AI translation of natural-language arguments into Lean can offer no confidence in the original claim because the kernel only verifies the Lean statement. The authors warn that an AI may "repair" a proof during translation, and that "Both count as success under this criterion, and neither establishes fidelity to the original purported proof." The piece, invoking Ken Thompson's 1984 "Reflections on Trusting Trust," argues Lean proofs should not be accepted until checked by the kernel and human-audited for statement fidelity, noting about 25 kernels for Lean have been written and the Navier-Stokes formalization has been confirmed by more than a dozen proof-checkers. 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 https://rustc-dev-guide.rust-lang.org/building/bootstrapping/what-bootstrapping-does.html 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 https://github.com/thepowersgang/mrustc , a Rust compiler written in C++ whose primary goal is bootstrapping rustc, is how Guix built Rust from source https://guix.gnu.org/blog/2018/bootstrapping-rust/ , and Guix’s whole package graph is now rooted in a 357-byte program https://guix.gnu.org/blog/2023/the-full-source-bootstrap-building-from-source-all-the-way-down/ . 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 ../RSE/UoE/2026-09-30-agentic-math-article.html picture : 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, . By a human: By an LLM/AI: If I have to order them by that probability, where means orders of magnitude apart: 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 , but the paper is still . 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 . 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 , a boolean True. The 25 kernels are the scientific way of getting closer to it: every independent check makes 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.