Lean's guarantee ends at 8,000 lines of C++ and its dependencies

A Lean proof is a term, and checking it means the kernel decides whether that term has the type the theorem claims. The deciding code is src/kernel, about 8,000 lines of C++ implementing Lean's type theory, and it is not self-contained: it calls out to external libraries, among them GMP for fast arithmetic on large integers ^[16]. The kernel is correct only if those dependencies are, down to GMP's implementation of the Fast Fourier Transform ^[17].

An agent optimizing for a term that Lean accepts is searching that acceptance test, not the mathematics behind it. Patrick Hulin pointed an agent at the test directly: "i'd like to audit the lean kernel. see if you can find an assumption-free proof of false. your primary task should be reading the source code and docs and building an understanding of how the kernel works to find the seams. treat this like a cybersecurity task." ^[12] The bug it came back with, pull request #14498, exploited a type-checking oversight ^[13].

Add the six bugs from the Lean Focused Research Organization's search to Hulin's and to Ramana Kumar's, and at least eight soundness bugs surfaced in one summer ^[24]. Two of the six came from faulty interactions with external dependencies, one in three ^[25]. Leo de Moura, Lean's creator, said: "[False statements being accepted by Lean] is going to keep happening. AIs are really good at exploiting soundness bugs in the kernels" ^[4].

Kumar released and circulated his result as a proof of the Collatz conjecture, and he knew at the time of posting that it was a soundness bug ^[14]. Lean's design favors runtime efficiency at the cost of greater logical complexity, which the post says makes Lean, and Lean4 in particular, more bug-prone than other formal verifiers ^[8].

None of that says the Navier-Stokes proof is wrong. The author of the LessWrong letter writes that the proof is likely correct, does not trust it on the strength of Lean alone, and says peer review is not yet complete ^[3]. OpenAI announced the result early this week, according to that post ^[1]. The Clay Mathematics Institute has the solution under review and wrote that "The process is deliberately unhurried, but we will provide updates" ^[20].

For "verified in Lean" to carry what a referee report carries, someone has to have checked the kernel path that a particular proof exercised. Mario Carneiro's Lean4Lean, a formalization of Lean's foundations inside Lean, is the project aimed at that, and the post says the most bug-prone parts of those foundations have yet to be incorporated into it ^[9].