数学家陶哲轩（Terence Tao）在其个人博客（terrytao.wordpress.com）发表文章《What mathematicians should know about the Lean Theorem Prover: reliability & AI》，发布时间为 2026 年 10 月 9 日。文章面向数学研究者，主题围绕 Lean 定理证明器的可靠性问题，以及它与人工智能之间的关系。
Lean 是近年来在数学形式化领域受到关注的交互式定理证明器。它的基本思路是：把数学定义、定理与证明写成计算机可以逐行检查的形式语言，由机器而非人工来核验每一步推理是否合法。随着形式化项目规模扩大，这类工具正在从逻辑学与计算机科学的小众工具，进入更广泛的数学研究视野。
文章标题点出了两条当前讨论的主线。第一条是可靠性。当证明被形式化之后，"这份证明是否可信"的问题，就从对论文的人工审阅，部分转移到对证明器内核、所依赖的数学库以及构建与运行环境的信任上——链条上任何一环出问题，都可能影响最终结论。对数学家而言，理解这种信任的边界，是使用此类工具的前提。
第二条是人工智能。大语言模型等系统已开始尝试生成数学证明，而形式化证明器提供了一条自动验证这些产出的可能路径；与此同时，模型输出与严格证明之间的差距也不断暴露。二者的结合被视为 AI 词典：AI for Math">AI for Math 的重要方向之一。
对关注 AI 与数学交叉方向的从业者来说，这篇文章的意义在于：它从一位数学家的视角出发，梳理了使用 Lean 时需要了解的背景与注意事项，有助于判断形式化验证在 AI 数学推理中能承担什么、又不能承担什么。