con-leche：用 Lean 证明自身一致的外部 Lean 检查器开源
burny_tech · x · 2026-09-11
Lean 官方账号介绍 con-leche——一个外部 Lean 检查器，其本身在 Lean 中被证明是一致的，即不会接受任何对 False 的证明。项目由 Joachim Breitner 构思，核心思路是允许检查器实现做额外工作（注解、检查），只要不破坏可靠性且让一致性证明更容易。该项目已有实际用途：单线程约 20 分钟可处理完一个 mathlib 导出，代码托管在 GitHub（leanprover/con-leche）。对形式化验证与可信证明检查感兴趣的读者值得关注。
所属事件:Lean 开源外部检查器 con-leche，自身一致性获形式化证明(2 条相关)→
「研究」频道最新
- DARPA 启动 expMath 计划，研究者分享数学猜想自动发现工作 — wellecks · 2026-09-11
- ETH 团队开源 VidMap：利用时序结构做视频三维重建，ECCV 2026 入选 — rsasaki0109 · 2026-09-11
- 中国 AI 智能体眼科诊所落地，Nature Medicine 总结真实世界经验 — EricTopol · 2026-09-11
- ValsAI 发布 RSI Index:首个第三方基准测试模型自研继任能力 — JenniferHli · 2026-09-11
- Caltech 本科生办 AI 数学竞赛遭质疑,组织者公开回应争议 — Singularitarian · 2026-09-11
- 前 NeurIPS 审稿人赞 YOCO：设计干净、消融扎实的好论文 — donglixp · 2026-09-11