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 条相关)→
「研究」频道最新
- OpenSIR 自博弈框架：LLM 无需训练数据自学数学推理 — PMinervini · 2026-10-28
- 网友玩坏可解释性:找到了让 Qwen「发疯」的神经元 — sebkrier · 2026-10-28
- 不开向量检索也能拿 86.67%,开源记忆层 Mind 挑战 embedding 必要性 — GabrielMartinMoran · 2026-10-28
- 提议：给每篇 arXiv 论文找最短复现 prompt,度量真实信息增量 — tak3sh8 · 2026-10-28
- Piano2Pop：无需对齐监督，把钢琴 demo 自动扩展成完整流行歌 — affige_yang · 2026-10-28
- RAX让真机器人探索2小时自学技能，再把技能写成代码复用 — du_yilun · 2026-10-28