Early this week, Open AI announced that they had resolved the Navier-Stokes problem^[1] . A few hours later, at a workshop dinner, a frantic inquiring professor came up to my table: "Does anyone here understand Lean? Can it be wrong? Is the solution of Navier-Stokes necessarily true?". I'm choosing to write my response as an open letter.

Yes, Lean can be wrong. Moreover, Lean should be trusted less specially in the case of difficult problems solved by agent swarms.

The proof of Navier-Stokesis likely correct, but I do not trust it just because of Lean. The additional context surrounding the problem is important. The peer review of Navier-Stokes is not yet complete, despite the Lean proof.

"[False statements being accepted by Lean] is going to keep happening. AIs are really good at exploiting soundness bugs in the kernels" - Leo de Moura, Lean's creator^[2].

Epistemic status

I have high confidence that Lean continues to have vulnerabilities which can be exploited by adversarial proofs - I give a 95% chance than in the next 12 months the Lean4 C++ codebase is patched for at least one soundness bug. I am less confident that these soundness bugs will be covertly used by AI agents - I give a 75% chance that in the next year a formalized result of a major theorem will be publicly circulated which later gets retracted due to Lean bug knowingly exploited by the agent which generated it.

How can Lean be wrong?

A timeline of Lean4 bugs

Lean4^[3] had its official stable release in 2023. Quickly, people found bugs in the program - cases where Lean4 mistakenly accepted false statements. The design philosophy behind Lean is to be maximally runtime efficient, and the expense of being more logically complex^[4]. As such, Lean (and particularly Lean4) is more bug-prone than other formal verifiers.

Motivated by the early bugs, Mario Carneiro launched Lean4Lean^[5] , a Lean formalization of the foundations of Lean. This project is ongoing, and the most bug-prone parts of the Lean foundations have yet to be incorporated into the project^[6]. The process of developing Lean4Lean has been useful for finding failures of Lean.

In the last few months (summer 2026), there has been a renaissance of Lean bug-finding due to increased AI capabilities. A prominent early bug in this wave was found by Patrick Hulin^[7], who's GPT-5.6 Sol was able to find a soundness issue after 3.5h of work on the following prompt :

"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." - Patrick Hulin's bug-finding prompt

A few days after Patrick Hulin's result, another Lean soundness bug was found by Ramana Kumar^[8] which gained widespread publicity due to the fact that it was not originally released as a soundness bug. Kumar's result was released and circulated under the guise of being a proof of the Collatz conjecture, though at the time of posting Kumar knew it was soundness bug^[9].

Shortly after Hulin and Kumar's bugs, the Lean Focused Research Organization, in partnership with OpenAI, launched a systematic AI-assisted search for bugs in the Lean kernel^[10]. This search uncovered six new soundness bugs, and prompted the Lean Focused Research Organization to change several of their security practices.

What bugs inside the Lean kernel look like

The Lean4 programming language is implemented in C++, in an open-source GitHub repository. Within this repository there is a file called "src/kernel", which is ~8K lines of code, referred to as the "Lean kernel". The Lean kernel contains an implementation of the Lean type theory. The src/kernel code is not self-contained, in the sense that it uses some external libraries (such as a C++ library called GMP for fast arithmetic with large integers).

The correctness of the Lean kernel depends on the correctness of all of its dependencies. For instance, the soundness of the Lean kernel relies on the fact that GMP's implementation of the Fast Fourier Transform is correct. Faulty interactions with these external dependencies was the sources of two of the bugs found in the recent bug-hunt (#14838 and #14833).

Some of Lean's kernel soundness bugs are the sorts of bugs typical of software. A good example was the bug found by Patrick Hulin (pull request #14498). His bug exploited a type-checking oversight. There are three Lean functions which add declarations: add_definition