con-leche: an external Lean checker proven consistent (in Lean) goes open source
burny_tech · x · 2026-09-11
leanprover introduced con-leche, an external checker for the Lean theorem prover that is itself proven (in Lean) to be consistent—it will not accept a proof of False. Conceived by Joachim Breitner, its core idea is to let the checker do extra non-essential work (annotations, checks) when that makes the soundness proof easier. It's practically usable: it processes a mathlib export in about 20 minutes on a single worker thread. Source: github.com/leanprover/con-leche.
Related event: Lean Releases con-leche, an External Checker Proven Consistent Within Lean(2 posts)→
More from Research
- DeepMind researcher: all of mathematics will soon be formalizable, with agents hunting proofs — ChrSzegedy · 2026-10-28
- A fine-tuned 'cat obsession' control fools every AI welfare criterion — MirrorEthic_Anchor · 2026-10-28
- Sweeping every Qwen3-8B neuron, rated for weirdness by Haiku — Sauers_ · 2026-10-28
- Kevin Buzzard: Lean formalization revealed errors in theorems by 4 Fields medalists — Machine Learning Street Talk · 2026-10-28
- Follow-up repo machine-verifies Hamiltonian cycle results on top of OpenAI/Anthropic ETH refutation claims — xennygrimmato_ · 2026-10-28
- DiscoTrace wins EMNLP 2026 Best Paper: LLM answers lack humans' community-specific rhetorical diversity — TuhinChakr · 2026-10-28