数学家需要了解的 Lean 定理证明器：可靠性与 AI

过去，研究人员必须依靠人力将论文证明转写为形式化证明。例如，关于三维球堆积的开普勒猜想，其形式化证明耗费了约20个人工年才完成，包含约50万行证明脚本。多年来，我们许多从事形式化工作的人一直梦想找到方法，为这一过程带来更高的自动化程度。自动形式化就是这一梦想的实现。自动形式化是指用AI对数学进行形式化。AI读取论文（比如pdf或tex文件），然后输出Lean或其他证明助手的形式化证明。

自动形式化在2026年已成为切实可行的现实。从2025年晚春和夏季开始，研究人员对自动形式化越来越乐观。以下是一些里程碑。

2025年9月，Math Inc. 完成了素数定理的准自动形式化。之所以仅仅是“准”，是因为每当AI卡住时，人类必须介入给出进一步指导。

2026年1月，J. Urban发布了一篇arXiv预印本“130k lines of formal topology in two weeks”，给出了在基于集合论的证明助手中对Munkres拓扑学教材大部分内容的自动形式化。

2026年3月。在宣布完成8维形式化大约一周后，Math Inc. 宣布了对24维球堆积问题的自动形式化，遵循的是Viazovska及其合作者的证明。该项目生成了约50万SLOC（源代码行数），后来经过代码精简（golfing）缩减到约20万行。

2026年5月，Meta/Facebook Research的一个团队在一个名为ATLAS的项目中自动形式化了26本数学教材的大部分内容。

此后，大量定理已被自动形式化。尤其值得注意的是Anthropic于9月4日宣布的费马大定理的自动形式化。该项目在11天内生成了1300万行Lean代码。OpenAI于9月8日宣布的带强迫项的Navier-Stokes爆破，同时附带了该定理在Lean中的自动形式化。

展望未来，Urban在1月表示：“我们相信，无论使用哪种证明助手，(自动)形式化在2026年都可能变得相当容易且无处不在。”自动形式化项目已在各种证明助手中使用各种LLM完成，但我们重点关注Lean。“对[Jesse] Han来说，它代表着更多：数学中一场革命性转变的开端，在这种转变中，极大规模的形式化将变得司空见惯”（IEEE Spectrum）。Jared Lichtman于2026年9月8日宣布启动MAP（Mathematics Autoformalization Project），旨在将“所有已知数学转化为形式化代码”。他请我们想象接下来的那一万亿行代码。