多位数学家谈如何形式化全部数学：AI 自动形式化的风险与路径
How to Formalize All of Mathematics
Jeremy Avigad、Kevin Buzzard 等七位数学家在客座文章中回应 OpenAI 近期发布后出现的“尽快形式化全部数学”呼声，认为大规模协调的形式化若做得好可扩展数学探索，做得差则浪费资源并可能造成长期损害。
（本文为客座文章，由 Jeremy Avigad、Kevin Buzzard、Johan Commelin、Rémy Degenne、Kim Morrison、Oliver Nash 和 Adam Topaz 撰写。）
数学家们对上周 OpenAI 重大发布的反应从兴奋到沮丧不一而足，但有一点是明确的：AI 在证明定理方面已经变得非常出色，无论是形式化还是非形式化。形式化领域的成功让 AI 爱好者们宣称，现在正是将全部数学形式化、作为留给后世的遗产的时候。
我们赞同这一提议。我们认识到新技术在数学推理方面的力量，也欣赏它们能为我们所熟知和热爱的学科做出的贡献。总体而言，我们对 AI 能发挥的作用持乐观态度，但我们对最近一些呼吁尽快将一切形式化的声音深感担忧。如果做得好，一场大规模、协调一致的形式化努力可以极大地拓展数学探索与发现。如果做得不好，往好了说是在浪费资源；更可能的是，它会造成持久的损害。
我们更希望看到形式化工作做得好。因此，本文旨在阐明我们的担忧，描述我们在 AI 与形式化方面的一些经验，并提出一个积极的愿景：我们如何共同努力，走向一个所有——或几乎所有——数学定义、定理和证明都配有形式化表示的世界，并让这些成果帮助数学蓬勃发展。
正如如今 AI 在数学中的角色是一个充满争议的话题，它在形式化中的角色同样如此。专家级形式化工作者对 AI 的态度之广，与更广泛的数学家群体中的态度之广不相上下。我们深知，我们一些最亲密的朋友和同事——我们高度重视并尊重他们的意见——强烈反对使用 AI 进行大规模形式化。我们在此所说的任何内容都不应被视为代表我们所属的任何组织或社区的观点。
担忧
让我们从这样一个观察开始：如果没有人使用，形式化成果就没有多大价值。去年二月，当 Math, Inc. 试图劫持一个项目来形式化 Maryna Viazovska 的高维球堆积结果时，它令人印象深刻地展示了这项技术的能力，但除此之外，它对数学毫无贡献。原项目团队继续准备 8 维结果的高质量形式化，并很快发现清理 AI 生成的代码得不偿失；事实证明，更好的做法是丢弃这些代码，从头正确做起，同时仍然借助 AI 的大量帮助。
当 Anthropic 宣布 Claude 用 11 天编写的 1300 万行代码形式化验证了费马大定理时，Kevin Buzzard 欣然称赞了这一成果，同时也声明他无意终止自己正在进行的对一个更现代证明的形式化工作。再一次，尽管这一成就令人印象深刻，但这段 AI 生成的代码可能几乎没有持续价值。
这里发生了什么？这些定理本身并没有受到严重质疑，因此形式化成果的价值完全在于我们从中获得的、超越单纯正确性的东西。我们想要形式化一切，是因为我们希望利用这些形式化成果去做更多数学，并且比没有它们时做得更好。我们想要思考可能的推广，探索数学不同分支之间的联系，并考虑意想不到的应用。我们想要重构和改进我们的知识：手工形式化的部分乐趣来自于意识到我们可以调整概念，使其更优雅、更高效、更符合我们的目的。知识只有在有助于我们的理解时才值得拥有；形式化的价值来自于我们使用和与数据交互的能力。
当 OpenAI 宣布 了在有限时间内爆破的 Navier–Stokes 方程解时，自然语言证明附带了 Lean 形式化。与之前的例子相比，正确性信号在这里发挥了关键作用：现在似乎很少有人怀疑该解是正确的，尽管自然语言证明大多难以理解。尽管如此，OpenAI 还是引起了数学界的愤怒，原因是人们担忧它如何获得该结果、思想的来源和归属，以及担心仅关注正确性会阻碍千禧年大奖旨在促进的探索和理解。因此，即使在这里，未经修饰的形式化成果也是喜忧参半。OpenAI 后来的 发布 包含了惊人且重要的数学，同时显示出对读者和构建理解的显著漠视（一些结果已被撤回，许多非正式/正式配对在微妙或显著的方式上存在分歧，而且大多数非正式写作令人难以理解）。
这解释了我们的担忧。如果花费数百万美元形式化数学，结果却是无人使用的库，那将是资源的可怕浪费。更糟的是，该项目可能会抑制良好的研究和 AI 的高效使用，破坏研究赖以生存的社会规范和实践，并使该领域倒退数十年。一次重大失败将使以后难以甚至不可能恢复。对现有结果的糟糕形式化比完全不形式化更糟。
积极方面
大型实验室的一些成果做得很好：OpenAI 的 单位距离猜想 工作，以及 Anthropic 关于 黎曼 zeta 零点密度 的工作尤为突出。它们展示了令人印象深刻的新能力，促进了对问题的理解，社区随后在其工作基础上继续发展。这些是实验室如何做出积极贡献的例子，我们邀请研究社区与实验室之间建立进一步的建设性伙伴关系。
优秀的正式库将使我们对于数学研究未来的积极愿景成为可能。人类、AI 和 Lean 语言协同工作。如今，AI 在数学研究的许多方面都极为强大。使用交互式定理证明器的研究者已经理解并欣赏拥有一个能够检查1证明有效性的编译器的力量。这些工具结合在一起，效果惊人。AI 在工作时会生成形式化证明，不断对照 Lean 编译器检查这些证明，并自动剔除错误的推理。要实现这一愿景，我们需要一个前所未有规模的高质量、全面的形式化数学库，以便数学家能够在研究前沿有效地工作。虽然我们是以研究数学家的身份写作，但我们必须牢记，这一愿景超越了数学，有可能加速工程和科学领域的研究。只有当我们做对了，这种回报才能证明投入大量资源是合理的。
迄今为止的经验教训
我们已经论证过，如果我们想用 AI 来帮助形式化，就需要解决对齐问题的一个特例，即确保形式化库满足社区的数学目标。我们相信，解决这一特例将为我们提供有力的经验教训，告诉我们如何更普遍地以安全、可靠且符合我们价值观的方式使用 AI。
我们该怎么做？我们没有人能确定：这正是前沿生活既令人兴奋又令人不安的部分原因。但总的来说，我们都有使用 AI 进行形式化的经验，任何认真的努力都应该关注我们迄今为止学到的东西。特别是，我们想提请注意以下项目。
Mathlib 是一个开源、社区驱动的库，支持形式化数学生态系统，并获得了 2026 年让-皮埃尔·德迈利数学开放科学奖。它由 65 名审阅者和迄今为止 950 名贡献者组成的团队管理。由于它强调高质量、可信赖的代码和人工管理，Mathlib 稳步增长，但比 AI 生成的库慢。出于同样的原因，它一直是我们学习如何更好地形式化的主要场所。
Formal Conjectures 是一个协作项目，旨在收集开放问题的形式化陈述。这是一项社会性事业，需要讨论、审阅和审计。AI 可以是有用的辅助，但目标是获得各学科重要开放问题的可信陈述。我们应该鼓励宣布形式化的项目尽可能使用现有的经过审核的问题陈述。
《数学年刊》挑战。 Kevin Buzzard 正在领导一个项目，旨在陈述（但不证明）近期《数学年刊》（以及后来的其他顶级期刊）中的所有定理。这里的障碍是缺失的定义，而该项目的要点之一是，它激励对领域领军人物在实践中使用的定义进行良好的形式化。这样的项目帮助我们将精力集中在回报最高的地方。
Tau Ceti 正在构建一个大型的连贯形式数学库，由 Lean FRO 和 Mathlib Initiative 孵化。虽然结构上与 Mathlib 相似，但所有贡献都由 AI 编写，然后由其他 AI 使用标准评分标准进行对抗性审查。这些贡献遵循由数学家和形式化专家策划的路线图。审查标准包括适当的通用性、通过复用现有材料避免重复、文档和命名约定。Tau Ceti 在没有任何重复的情况下扩展 Mathlib，并遵从那里做出的所有设计决策。可以通过编写路线图或提供推理2来为 Tau Ceti 做出贡献。Tau Ceti 现在比 Mathlib 稍大（300 万行代码），并且正在快速增长。最近的成果包括 Riemann-Roch、Schur-Weyl 对偶、Jordan-Brouwer 分离、Rellich-Kondrakov 紧性 和 Chebotarev 密度。
Formal Frontier 是 Mathlib Initiative 的一个项目，构建将源文本转换为相互关联的形式库的流水线。它使用一个交互的 AI 代理社区，可以指示这些代理形式化特定文本。该系统在设计时考虑了可扩展性，因此可以摄取数千本教科书。现在有 41 个已发布的库（例如关于射影群、环面理想和同调代数），包含约 20 万行代码。除了提供管理代理群的基础设施外，Formal Frontier 项目还为大型 Lean 项目编写了一个构建服务器。Formal Frontier 最近的亮点包括 毛球定理、Kaplansky 射影模定理、Bass 稳定范围定理、Tate 周期性 和 谱空间的 Stone 对偶 的形式化。
Formal Frontier 和 Tau Ceti 都使用代理和对抗性审查，但它们在驱动因素和输出结构上有所不同。Tau Ceti 使用由专家策划的路线图，并构建一个单一的连贯库。Formal Frontier 主要是一个从源到库的流水线。两者都坚持认为，只有其他人能够在其基础上构建时，形式化才有价值。我们预计未来的自动形式化项目将建立在两种方法之上。
Palomar 是一个形式数学项目的在线注册表。Palomar 的目标是索引针对特定结果的形式化项目，但不一定希望成为通用库的一部分。许多这样的结果最近被“倾倒”在 GitHub 上，解释或信任它们可能非常困难。Palomar 通过要求其索引的每个项目具备两个特征来解决这个问题。首先，项目必须包含一个 formalization.yaml 文件，这是一个元数据文件，包含对形式化内容的自我评估描述、如何形式化（例如仅由人类、与 AI 合作，或由 AI 自主完成），以及与其他工作的关系，以及基础非正式研究的作者如何参与该项目。其次，项目必须包含一个 Comparator 设置，这使得审计该陈述所证明的内容变得更加容易。
Mathlib、Tau Ceti 和 Formal Frontier 追求共同的价值观。这些并非自动形式化所特有，而是适用于所有形式化库的原则。Mathlib 社区最近发布了一份关于价值观的文件，这是我们自己列表的起点。
- 遵从人工维护的库，尤其是 Mathlib；遵循它们的设计原则和代码规则，并持续重构以采纳它们的决定。
- 优先考虑全面性和广度。这些必须先于深度，但最终会促成深度。
- 避免重复。推广定理以实现最大程度的复用。
- 按照商定的标准，公开审查新增内容。
- 自由发布。库应当是开源的、可互操作的、可探索的。
- 保持最新。确保与 Lean 和 Mathlib 的每个版本持续兼容。
- 对变化保持开放心态。如果发现了更好的方法，永远都不算晚。
- 记录并组织。文件应当连贯、系统化组织，其内容必须被记录。
- 链接到现有文献。数学家应当能够信任并验证库中描述的概念具有预期的含义。
- 设定标准，并达到标准。产出低质量或未经审查的代码，并声称或希望“以后再清理”，是适得其反的。
Mathlib 通过其审查流程和社区讨论来践行这些价值观。Tau Ceti 和 Formal Frontier 在驱动它们的代码和提示词中，以及在社区编写的规划文档中，将这些价值观具体化。
前进之路
在三年内，甚至可能更快，大部分数学都可以被形式化，使数学家能够探索、构建并利用形式化库。这将显著扩展我们发展和发现新数学的能力。Lean FRO 致力于确保 Lean 能够支持这种规模的项目。实现这一雄心勃勃的项目将需要多种额外的支持和社区参与：
来源：Hacker News · xenaproject.wordpress.com