“Don’t trust Lean4 alone” by Milo Moses

Early this week, Open AI announced that they had resolved the Navier-Stokes problem . 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. 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 [...] --- Outline: (01:09) Epistemic status (01:43) How can Lean be wrong? (01:46) A timeline of Lean4 bugs (03:55) What bugs inside the Lean kernel look like (06:20) Bugs outside the kernel (06:58) A mechanism for Lean exploitation (08:05) Outlook The original text contained 12 footnotes which were omitted from this narration. --- First published: September 16th, 2026 Source: https://www.lesswrong.com/posts/jgmmMa7AqJNausrqx/don-t-trust-lean4-alone --- Narrated by TYPE III AUDIO.