The Lean Proof Assistant Now Ships With Four Extra Kernels: con-leche Was Written and Proven Consistent by Claude, and lake check --paranoid Rechecks With All of Them

After AI found holes in the kernel

Lean is a proof assistant widely used by mathematicians and formal verification teams, and the component that has the final say on whether a proof is correct is its kernel. Leonardo de Moura, co-founder and chief architect of the Lean FRO, wrote on his blog on October 15 that AI agents are very effective at finding vulnerabilities in software, Lean's kernel included; the team published postmortems on August 1 and August 24. The response has three parts: strengthen the official kernel, add new kernels, and make it easy to recheck work with external ones.

Lean v4.35.0, released on October 12, brings lake check: it exports the whole project and rechecks it in a sandbox with leanchecker, the official kernel without the surrounding machinery. lake check --paranoid additionally runs the four kernels that now ship with Lean, nanoda, lean4lean, con-leche and con-ron, plus a build of the official kernel with a hardened memory allocator, which turns memory corruption into a checked abort instead of a silently wrong answer.

A kernel Claude wrote

con-leche is the first Lean kernel written in Lean and proven consistent. According to de Moura, it was implemented and proven consistent by Claude (Fable and Opus) under heavy supervision by Joachim Breitner at the Lean FRO. "Consistent" here means every environment it accepts has a model in set theory, following Mario Carneiro's model of Lean's type theory; the proof itself is checked by the official kernel and assumes the set theory used is consistent. That rules out a whole class of bugs, programming mistakes in the kernel implementation, with no performance penalty: on the full Mathlib export it executes 0.69x the instructions of the official kernel and finishes in about 100 seconds on eight threads.

It can still be affected by bugs in Lean's compiler and runtime. So Breitner used AI to translate con-leche into Rust, producing con-ron, and used Aeneas to prove that the Rust version refines the same checking algorithm. The same bug is unlikely to exist in both toolchains, so a proof that passes both is on firmer ground.

Scale is the next bottleneck

De Moura offers some numbers: Anthropic's FLT (Fermat's Last Theorem) formalization is over 13 million lines, Mathlib has 2.5 million, and the community is already proposing math libraries in the billion-line range. The current way of rechecking with external kernels will not scale to that, and the team is working on binary export formats and incremental checking. For now his advice is simple: run lake check --paranoid on your own project, and if the kernels disagree about a proof, report it to the Lean FRO.