Lean 4.35 ships con-leche, a proof checker Claude wrote and proved consistent

What the Lean FRO shipped

The Lean proof assistant now comes with a way to recheck any project against five independent proof checkers at once, and one of them was written by an AI model that also proved it cannot be tricked into accepting a proof of False. In a post on 15 October 2026, Leonardo de Moura, chief architect and co-founder of the Lean FRO, the nonprofit that develops Lean, said Lean v4.35.0 ships a new lake check command and four extra kernels: nanoda, lean4lean, con-leche and con-ron.

Con-leche is the headline. De Moura calls it the first kernel for Lean written in Lean and proven consistent, and says it was implemented and proven consistent by Claude, naming the Fable and Opus models, under heavy supervision by Joachim Breitner at the Lean FRO. Its GitHub repository is public under the Apache 2.0 licence, and Breitner writes in the README that he considers the checker production ready.

The release notes date Lean 4.35.0 to 12 October. The main new tactic feature is vcgen, a faster successor to the mvcgen verification condition generator, but the checking tools are what matter for anyone who relies on Lean to vouch for proofs they did not write themselves, including proofs produced by AI systems.

Why Lean needed more than one kernel

A kernel is the small program at the bottom of a proof assistant that decides whether a proof is accepted. Everything else, from tactics to automation, can be wrong without harm as long as the kernel is right. A bug in the kernel is different: it can let a proof of False through, and from False anything follows.

That risk stopped being theoretical this summer. In an August postmortem, de Moura described a bug hunt run with Daniel Selsam at OpenAI, who used OpenAI internal models against the official Lean kernel and runtime between 30 July and 20 August, when the model reported it could find no more issues. The model got the official kernel to accept a proof of False through several kernel bugs, then turned to the runtime: it overflowed the reference counter of an object used by the kernel to corrupt memory, and it noticed that Lean's Linux builds used GMP 6.1.2 rather than 6.3.0 and crafted a proof of False from a known bug in the older library. Lean v4.33.1, released on 21 August, fixed all of them. The postmortem notes that none of the groups using publicly available models reported any bugs.

The lesson the FRO drew is that a single kernel is a single point of failure, and that AI-generated proofs should be treated as potentially malicious input. That matters as AI labs lean on Lean to certify results, from OpenAI's batch of 722 machine-written maths manuscripts to DeepMind's AlphaProof Nexus work on Erdős problems. Checking the same proof with independently written kernels means a bug has to exist in all of them, in the same place, to slip through.

What con-leche proves, and what it assumes

Consistent, in de Moura's words, means that every environment con-leche accepts has a model in set theory, following Mario Carneiro's model of Lean's type theory. In practice that means the proof rules out the class of bugs that come from programming mistakes in the checker itself.

The repository states the result two ways. The main corollary, a theorem called no_False_declaration, says that an export file containing a theorem whose statement is False, with arbitrary declarations around it, will be rejected. The meaning of False is hard-coded, so redefining it does not help an attacker. The stronger main theorem, model_exists, says every accepted environment has a model, so every accepted theorem statement is true in that model. The README says the fast byte-level parser is proven equivalent to a naive reference parser and is covered by the corollary.

The proof is checked by the official Lean kernel, and it rests on an assumption about set theory: roughly, ZF without the axioms of infinity and choice plus an infinite chain of Grothendieck universes, which the repository instantiates from the hypothesis of infinitely many inaccessible cardinals used in Carneiro's analysis. Mathematicians will recognise this as a standard, though not trivial, foundational assumption.

The design has a cost that the README is candid about. To make the proof go through, con-leche does extra type comparisons that a checker does not strictly need, which Breitner calls the certification tax. A trusted mode skips those checks so the tax can be measured. Con-leche accepts only Lean's three standard axioms, rejects any other axiom, and will complain if sorry is actually used.

Claude wrote it, a human steered it

The repository is unusually open about who did what. Its README says the code was implemented and proven consistent by Claude under Breitner's supervision, points readers to the git history for the detours and dead ends, and adds that the README itself is human written, with AI only copy-editing, fact checking and filling in numbers, and that it is probably the only human-written thing in the repository. An AI-written write-up of the core proof idea is published alongside it.

The second new verified kernel came the same way. Breitner used AI to translate con-leche into Rust, then used Aeneas, a tool for verifying Rust code in Lean, to prove that the Rust version, con-ron, refines con-leche's checking algorithm. The point is defence in depth: con-leche's proof says nothing about bugs in Lean's own compiler or runtime, including its bignum arithmetic, but a matching bug is very unlikely to also exist in the Rust compiler and runtime.

This is a different kind of AI result from the headline-grabbing proofs of the past few months, such as the disputed Navier-Stokes proof or Intern-S2's work on the Ghys conjecture. Here the model built verification infrastructure, and the result can be checked mechanically by the existing kernel rather than taken on trust.

Is the verified checker slower?

Not according to the project's own measurements. De Moura says that on the full Mathlib export con-leche executes 0.69 times the instructions of the official kernel and checks the whole library in about 100 seconds using eight threads. The PERF.md file behind that figure records 7.05 trillion instructions in verified mode against 10.26 trillion for the official v4.33.0 kernel on a Mathlib export of about 691,000 declaration records, with the trusted mode at 6.40 trillion. On Lean's core library the gap is smaller, 408 billion against 440 billion.

Not every test favours it. On one test stream, grind-ring-5, con-leche used about 1.2 times the official kernel's instructions. The measurements were one run per cell on a shared 96-core AMD EPYC machine on 13 October, so they are an indication rather than a controlled benchmark, and AI Lookout did not rerun them.

How to use lake check

For most users the change is a single command. Plain lake check builds a project's default targets, exports them, replays the export through leanchecker, the official kernel stripped of surrounding infrastructure, and fails if anything uses an axiom other than the standard ones. Adding the paranoid flag runs lean4lean, nanoda, con-leche and con-ron as well, plus a build of the official checker with a hardened memory allocator that turns memory corruption into a checked abort, and the project passes only if every checker accepts it.

Both lake check and the new lake comparator command, which checks that a solution proves exactly the theorem statements in a challenge file using only permitted axioms, treat the project as untrusted. The build and export run inside a bubblewrap sandbox that hides the home directory and allows network access only for dependency resolution, and the kernel runs in a separate process. The sandbox is Linux-only for now, and it can be switched off with a flag pointedly named inadvisably-no-sandbox. Exports made elsewhere can be checked with a from-export option.

The FRO is asking for feedback. If the kernels disagree about a proof, de Moura wants to hear about it at contact@lean-fro.org. The release also closes two more ways an extremely large input could cause a use-after-free in the official kernel, plus a related threading fix; kernels not built on the Lean runtime were not affected.

The scaling problem ahead

The post is frank that the current approach will not keep up. De Moura lists Anthropic's FLT (Fermat's Last Theorem) development at over 13 million lines of code, Mathlib at 2.5 million, Tau Ceti at over 3 million and growing, and a General Courtade-Kumar theorem repository above 50 million, and says the community is writing proposals for libraries of more than a billion lines. External checkers that reread a full text export do not scale to that, so the FRO is working on binary export formats and incremental checking.

More verification is coming. The FRO expects lean4lean, which closely follows the official C++ kernel, to be verified in the next few months, giving Lean three verified kernels. Arthur Adjedj is carrying out a kernel renovation plan, with Breitner updating con-leche and its proof to match so no new holes appear, and the FRO wants users to be able to plug their own kernels into lake check.

Limitations

A consistency proof is not a guarantee that a checker matches what users mean. Con-leche's theorems are about its own model of Lean's type theory, and the README invites readers to check for themselves that the driver code does what the main corollary describes. The proof assumes the consistency of the underlying set theory, and accelerated arithmetic on natural numbers still relies on Lean's runtime, which the README names as a possible source of unsoundness.

The claims about Claude's role come from the Lean FRO and the repository; Anthropic has not published its own account, and the git history is the evidence for how much was done by the model. Performance figures are the project's own single runs. And lake check only helps people who run it: a proof posted online with a Lean file attached is only as trustworthy as the checks someone actually performed on it.