Thomas Hales · 陶哲轩博客客座文章 · 阅读原文
原始来源：Thomas Hales · 陶哲轩博客客座文章（terrytao.wordpress.com）
发现渠道：Hacker News
这篇刊于陶哲轩博客的客座文章，作者是 Thomas Hales，讨论数学家该怎样理解 Lean 的可靠性。关注点不只是一份证明能否被软件接受，还包括检查内核、独立交叉检查，以及形式系统所依赖的理论基础。Hales 重视形式化证明的进展，同时希望更多研究者参与基础理论工作。在文章结尾，他还提出：如果通向一致性的唯一已知路径，是缺少人类阐释的 AI 形式化证明，我们仍不能完全满意。下文保留这句话及其讨论语境。
可信度 65 · 重要性 72 · 新颖度 66
技术与主题
AI 编程 · 评测与基准 · 推理能力 · Formal Verification · Theorem Proving · Lean
Thomas Hales
博客明确标注为 Hales 客座文章；下面短引来自正文结尾的可靠性讨论。
忠实转述（非原句）：他的要求不止是检查更多证明，也包括让更多研究者参与 Lean 的基础理论工作。即使一致性十分重要，它也不是理解和信任一个形式系统所需的全部。
编辑评读
检查器接受证明，意味着它满足了那套规则；规则所依赖的基础是否可靠，是另一个层次的问题。Hales 要求继续研究后者，并不等于他给出了 Lean 不可靠的反例。把这两件事混在一起，会把文章读成一篇它并不是的警告。
对 AI 工具还可以再问一步：交给检查器的，是否就是人原本想证明的命题？这是从文章延伸出来的问题。即使检查器没有错，形式化时漏掉一个条件，仍可能得到一份正确却不适用的证明。保留原始要求与形式化表述的对应关系，能帮助人检查这一处差异；不能只留最后的通过标记。
需要留意
- 文章包含作者对理论基础与未来风险的判断；本期未独立审查 Lean 内核或相关一致性证明。