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
- 9th VISxAI workshop on AI explainability opens call at IEEE VIS 2026 in Boston — leland_mcinnes · 2026-09-11
- Researcher calls for perturbation-based multi-agent studies over one-off swarm observations — sebkrier · 2026-09-11
- 100-agent experiment: when 9% of AI agents cheated, 24% blew the whistle on peers — jzl86 · 2026-09-11
- Should researchers drop their marginal papers? A call for an RCT — RishiBommasani · 2026-09-11
- Science Advances paper introduces Media Bias Detector to measure publisher bias at scale — duncanjwatts · 2026-09-11
- OpenAI reportedly aims its new internal model at Riemann and P vs NP — zephyr_z9 · 2026-09-11