con-leche: Claude-built Lean checker proved consistent
Confirmed
The takeaway
On Sept 10, 2026 Joachim Breitner (Lean FRO) released con-leche, an external checker for Lean proofs that is itself proven in Lean never to accept a proof of False, relative to a set-theoretic model (ZF-style set theory with a chain of Grothendieck universes).
Status
- Claim
Confirmed
- Our reporting
- High confidence
- Importance
- 3 of 5
- Last verified
- 10 October 2026
Your AI and this story
- GPT-6 Astra133 days after its cutoff
- Claude Opus 5.572 days after its cutoff
- Gemini 3.8 Flash163 days after its cutoff
- Grok 4.7102 days after its cutoff
None of these four assistants can know about it. The closest, Claude Opus 5.5, stops 72 days before it.
Key facts
- Released Sept 10, 2026 (Breitner on Mastodon: ‘I’m a bit childishly proud that I just released a Lean Checker with a formal consistency proof. I declare the summer of AI-found kernel implementation bugs to be over!’); repo github.com/leanprover/con-leche (created Aug 19, Apache-2.0)
- AI role (README): ‘It was implemented and proven to be consistent by Claude (Fable and Opus), under heavy supervision by Joachim Breitner at the Lean FRO.’ The README is ‘probably the only human written thing in this repository’
- Main corollary (ConLeche/MainTheorem.lean, theorem no_False_declaration): an export file containing a
theorem … : Falseis never accepted; main theorem model_exists: every accepted environment has a model in the assumed set theory - Assumed set theory: ZF without infinity and choice plus an ω-chain of Grothendieck universes (Tarski form); instantiated on Mathlib’s ZFSet from the ω-many-inaccessibles hypothesis of Mario Carneiro’s lean4lean-model analysis
- Design: implemented in Lean with its own term representation (not relying on the unverified C++ routines behind Lean.Expr); accepts only the three standard axioms; theorem bodies opaque; parser ‘agentic-hand-written’ and verified against a naive one
- Status (README): ‘practically useful … comparable performance to the official kernel’; published ‘when it was barely usable – able to process mathlib within reasonable memory usage’
- Context: Thomas Hales’s Oct 9 guest post on Terence Tao’s blog cites con-leche (‘code and proofs generated by Claude’) as checking mathlib after the summer 2026 soundness bugs, including an illicit Collatz disproof and an illicit Kepler proof; he notes its set-theoretic consistency claim ‘might suffice for all practical purposes, even if it differs in technical detail from the claim of Lean type-theory consistency’
What happened
After a summer in which AI systems found several soundness bugs in Lean’s kernel (see Lean kernel soundness bug #14576), Joachim Breitner of the Lean FRO had Claude write a new, independent checker for Lean export files together with a Lean proof that the checker is consistent: it can never accept a proof of False, and every environment it accepts has a set-theoretic model. Breitner supervised; per the README, the code and proofs are Claude’s (Fable and Opus models), and the git history shows the detours.
The guarantee is relative to the assumed set theory (universes/inaccessible cardinals) and to the parts of the program that the theorem covers; the README invites readers to check that the main function’s data flow matches the theorem.
Why it matters
Proof checkers are the trust anchor for the wave of Lean-verified AI mathematics (for example OpenAI’s October release, checked with Comparator). A checker whose own consistency is machine-proved, and which was largely written by an AI, is a direct answer to the summer’s kernel bugs. It was found late (Oct 9) through Hales’s blog post.
Sources
4 sources from 4 sites. Numbers match the chips in the text.
4 sources: 3 primary, 1 reaction
Primary
- GitHub: leanprover/con-leche (README)github.com, code
- Joachim Breitner on Mastodon (Sept 10, 2026)mastodon.online, official
- Lean Kernel Arenaarena.lean-lang.org, docs
Reactions
- Thomas Hales (guest post on Tao’s blog): What mathematicians should know about the Lean Theorem Prover (Oct 9)terrytao.wordpress.com, discussion
Changes
- Filed (primary sources: repo README and Breitner’s Mastodon post)