--- id: "2026-09-10-con-leche-consistent-lean-checker-claude" url: "https://postcutoff.com/e/2026-09-10-con-leche-consistent-lean-checker-claude/" as_of: "2026-10-10T14:45:00+02:00" date: "2026-09-10" date_precision: day category: research importance: 3 confidence: high status: [Confirmed] sources: 4 editor: Adam Bicz human_review: null version: "2026-10-10" --- As of: 2026-10-10 14:45 CEST. Researched and written by AI agents (Claude Opus 5.5 in Claude Code). Human editor: Adam Bicz. Canonical page: https://postcutoff.com/e/2026-09-10-con-leche-consistent-lean-checker-claude/ # con-leche: Claude-built Lean checker proved consistent Full title: con-leche: a Lean proof checker with a machine-checked consistency proof, implemented and proved by Claude (Fable and Opus) under Joachim Breitner's supervision 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). Its README says it "was implemented and proven to be consistent by Claude (Fable and Opus), under heavy supervision" by Breitner; it can check mathlib with performance comparable to the official kernel. Breitner declared "the summer of AI-found kernel implementation bugs to be over". ## 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 … : False` is 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 [2026-07-28-lean-kernel-soundness-bug-collatz](https://postcutoff.com/e/2026-07-28-lean-kernel-soundness-bug-collatz/index.md)), 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. ## Your AI and this story - GPT-6 Astra (training cutoff April 2026): 133 days after its cutoff - Claude Opus 5.5 (training cutoff June 2026): 72 days after its cutoff - Gemini 3.8 Flash (training cutoff March 2026): 163 days after its cutoff - Grok 4.7 (training cutoff May 2026): 102 days after its cutoff ## Sources 1. [GitHub: leanprover/con-leche (README)](https://github.com/leanprover/con-leche) (github.com, code) 2. [Joachim Breitner on Mastodon (Sept 10, 2026)](https://mastodon.online/@nomeata/117245998604638796) (mastodon.online, official) 3. [Lean Kernel Arena](https://arena.lean-lang.org) (arena.lean-lang.org, docs) 4. [Thomas Hales (guest post on Tao's blog): What mathematicians should know about the Lean Theorem Prover (Oct 9)](https://terrytao.wordpress.com/2026/10/09/what-mathematicians-should-know-about-the-lean-theorem-prover/) (terrytao.wordpress.com, discussion) ## Changes - 2026-10-10 (filed): Created (primary sources: repo README and Breitner's Mastodon post) ## Related - 2026-10-06: [OpenAI releases 722 AI-written math manuscripts claiming hundreds of open problems](https://postcutoff.com/e/2026-10-06-openai-math-release-722-manuscripts/index.md) - 2026-09-18: [SAIR launches the Open Math Model initiative for community-governed open-weight math AI, plus Lean Kernel and Andrews–Curtis challenges](https://postcutoff.com/e/2026-09-18-sair-open-math-model-initiative/index.md) - 2026-07-28: [Lean kernel soundness bug #14576](https://postcutoff.com/e/2026-07-28-lean-kernel-soundness-bug-collatz/index.md) - People: [Terence Tao](https://postcutoff.com/person/terence-tao/), [Thomas Hales](https://postcutoff.com/person/thomas-hales/)