Lean 推出外部验证器 con-leche,在 Lean 内证明自身一致性
AlexKontorovich · x · 2026-09-10
Lean 生态迎来新工具 con-leche(CONsistent LEan CHEcker)：一个外部检查器，其自身一致性在 Lean 内得到了形式化证明，意味着它不会接受对 False 的证明。项目由 Joachim Breitner(@nomeata)主导开发，为形式化验证的信任链提供了更强的保证。数学家 Alex Kontorovich 等人转发称赞。
所属事件:Lean 开源外部检查器 con-leche，自身一致性获形式化证明(2 条相关)→
「研究」频道最新
- Mandelbrot 集拼图结构在 Lean 中完成形式化计算,实拍级图表曝光 — geoffreyirving · 2026-10-28
- Geoffrey Irving 对 CSETH 突破给出 >80% 概率预测 — geoffreyirving · 2026-10-28
- 抗衰研究数据荒：Norn 募资 1500 万美元为 AI 备好训练数据 — juanbenet · 2026-10-28
- 研究员自曝置信度乌龙：把 SETH 当 CSETH，重估 P vs NP 赔率 — geoffreyirving · 2026-10-28
- Google 论文指出 softmax 标准实现藏两个数值 bug，引发形式验证讨论 — srush_nlp · 2026-10-28
- AI 提出的研究题 45/135 获专家认可有趣，覆盖数学物理等 — StanfordAILab · 2026-10-28