← Back to feed

OpenAI models found soundness bugs in Lean’s proof checker twice in August. Anthropic’s Claude fixed the underlying problem by writing a replacement kernel that is formally proven correct.

Lean v4.35.0, released October 15, ships four additional kernels alongside the official one. The standout is con-leche: the first Lean kernel written in Lean itself and proven consistent with set theory. Claude (Fable and Opus) implemented it under supervision of Joachim Breitner at the Lean Focused Research Organization. The proof of consistency was checked by the official Lean kernel.

What Triggered This

OpenAI’s internal AI models, working with Daniel Selsam, and Ramana Kumar’s AI-assisted work discovered soundness bugs in Lean’s kernel twice in August 2026 — documented in postmortems on August 1 and August 24. Soundness bugs matter acutely in formal verification: they mean the checker can accept a proof that does not actually hold. The response from the Lean team was to multiply checking, not just patch.

Four New Kernels

Lean v4.35.0 introduces four additional checkers accessible via lake check:

• nanoda and lean4lean: independently implemented kernels written in Rust and Lean respectively
• con-leche: Lean kernel written in Lean, proven consistent — implemented by Claude (Fable and Opus)
• con-ron: con-leche translated to Rust by AI, then formally verified by Aeneas

Running lake check --paranoid invokes all four external kernels plus a variant of the official kernel built with a hardened memory allocator that converts memory corruption into a checked abort rather than a silently wrong answer.

What “Proven Consistent” Means

Consistency here has a formal definition: every environment con-leche accepts has a model in set theory, following Mario Carneiro’s model of Lean’s type theory. It eliminates an entire class of bugs — implementation mistakes in the kernel code — without requiring trust in con-leche’s own authors.

The proof itself was checked by the official Lean kernel. It assumes the consistency of the set theory used in the model, which is the same foundational assumption underlying mainstream mathematics.

Performance

Con-leche executes 0.69 times the instructions of the official Lean kernel. On a full export of Mathlib — the main library of formalized mathematics, containing hundreds of thousands of theorems — it completes rechecking in approximately 100 seconds on eight threads. The official kernel is both slower and unverified against a formal consistency proof.

The Rust Layer

After the Lean implementation was complete, AI translated con-leche into Rust. That Rust code was then verified by Aeneas, a tool that proves Rust programs refine specifications written in Lean. The resulting kernel is called con-ron.

The practical effect of running both: the failure modes of con-leche are bugs in Lean’s compiler or runtime, and the failure modes of con-ron are bugs in the Rust compiler or runtime. It is unlikely the same bug exists in both. Checking a proof with both kernels provides high assurance that a verification failure in one cannot be silently hidden by the other.

Why It Matters

AI models have spent years generating proofs in Lean. They are now building the infrastructure that checks whether those proofs are sound. The August postmortems showed that the checker itself was a vulnerability surface. The response — AI-assisted implementation of a formally verified alternative — closes that loop.

The Lean FRO is treating the kernel as a component that must itself be verified, not just trusted. That shift has practical consequences for anyone relying on Lean-checked proofs in formal software verification, mathematics libraries, or cryptographic protocol specifications.