Leonardo de Moura · Lean 项目 · 阅读原文
原始来源：Leonardo de Moura · Lean 项目
发现渠道：Hacker News · 热点发现
获取渠道：原站公开正文
即使证明经过自动检查，人们仍需要知道：检查程序本身会不会接受错误对象。10 月 15 日，Leonardo de Moura 介绍 Lean v4.35.0 随工具链提供的独立检查路径：lake check 导出项目的声明，让去掉大量外围功能的官方 leanchecker 在沙箱中重新检查；使用更严格的模式，还能调用 nanoda、lean4lean、con-leche、con-ron 等不同实现。这样做把复杂的交互、编译和证明生成流程，与最终接受证明的检查工作进一步分开。
其中 con-leche 用 Lean 实现，并在集合论模型假设下证明其接受对象的一致性；con-ron 是 Rust 实现，借助 Aeneas 对检查算法建立对应的精化证明。项目同时使用不同语言和工具链，降低所有实现撞上同一类编译器或运行时问题的机会。作者披露 AI 在实现和证明过程中发挥了很大作用，同时强调 Joachim Breitner 的持续指导。这里有两层不能混淆：模型参与写出检查器，不意味着模型本身成了最终裁判；形式化证明也仍有其公理、模型和执行环境的信任前提。
可信度 65 · 重要性 88 · 新颖度 65
技术与主题
评测与基准 · 推理能力 · Lean · Proof Kernel · Aeneas · Formal Verification
s_Hogg
Hacker News 对这篇 Lean 发布说明的讨论。
忠实转述（非原句）：评论者承认自己没有完全理解这项工作，接着追问：如果负责检查的程序也需要被检查，这是否只是把检查器一层层往下接？
measurablefunc
回复上述问题；属于技术解释，未报告独立复现。
忠实转述（非原句）：回复者解释，多个检查器不太可能都含有相同错误，因此用更多内核检查，可以提高对证明或代码一致且正确的信心；这一解释仍以检查器正确性所需的集合论假设为条件。
编辑评读
这项进展把“我们相信这段证明”拆成了可检查的链条：待证明声明是什么，哪个小程序接受了它，关于这个程序的正确性又证明到了哪里。对使用 AI 生成数学证明的人，价值在于最终产物进入明确的验证边界。它不会自动证明题目的自然语言翻译无误，也不会替用户判断定理是否值得证明。
多实现交叉检查和形式化证明提供的保障不同。前者有助于暴露实现分歧，后者在声明的假设下约束程序行为；它们不能简单相加成“零信任”。原文也保留了工程边界：lean4lean 的完整验证尚未完成，大规模导出与检查仍有扩展问题。本次读到项目说明、证明思路和性能记录，未自行编译或复验整个数学库。