AI人工智能正在改变我们撰写形式化证明的方式

AI 将深度参与下一代证明辅助工具的构建，但工具优劣的核心标准不变：高表达类型、易读规范、强自动化、可编程生态、优质工具链、可扩展性；技术迭代是进步的标志，目标是推动形式化数学的实用化与普及化。

作者：莱昂纳多・德・莫拉（Leonardo de Moura）2026-2-18

译者：zzllrr小乐（数学科普公众号）2026-3-1

作者简介

莱昂纳多・德・莫拉（Leonardo de Moura）是亚马逊云科技（AWS）自动化推理小组的高级首席应用科学家。在业余时间，他投身于非营利组织 Lean FRO 的工作，担任首席架构师一职 —— 该组织由他与塞巴斯蒂安・乌尔里希（Sebastian Ullrich）共同创立，他对此深感自豪。他同时还受聘担任 Lean FRO 的董事会成员，积极为该组织的发展壮大贡献力量。

2023年加入亚马逊云科技之前，自2006年起，他曾在微软研究院（Microsoft Research）的 RiSE 研究小组任职长达 17 年，担任高级首席研究员。更早之前，他曾就职于美国斯坦福国际研究院（SRI International），担任计算机科学家。

他的研究领域包括自动化推理、定理证明、决策过程以及可满足性问题（SAT）与可满足性模理论（SMT）。他是多款自动化推理工具的主要架构师，其中包括 Lean、Z3、Yices 1.0 以及 SAL。

莱昂纳多在自动化推理领域的研究成果斩获了多项颇具声望的奖项，其中包括计算机辅助验证大会（CAV）奖、海法奖、埃尔布朗奖，此外，他还凭借 Z3 与 Lean 两次荣获美国计算机协会编程语言专业组（ACM SIGPLAN）编程语言软件奖。他的研究成果也被《纽约时报》，以及《连线》、《量子杂志》、《自然新闻》、《科学美国人》等众多科普期刊报道。

如今，语言模型只需极少的人工指导，就能生成数千行经过验证的数学证明代码，且相关成本还在持续下降。这一突破令人振奋，同时也引出一个自然而然的问题：当人工智能承担更多证明工作时，证明辅助工具的选择会起到怎样的作用？

我认为答案是：它的重要性非但没有降低，反而愈发凸显。

证明辅助工具绝非仅服务于人工智能的工具，它更是人类与人工智能协同工作的核心环境。人类需要在其中查阅定义、理解定理表述、指导证明策略，并基于已验证的结论进行拓展；人工智能则需要高效生成证明、从反馈中学习，并借助自动化能力提升效率。一款设计精良的证明辅助工具能够同时满足双方的需求，而随着人工智能在证明工作中占据更大比重，那些促成这种高效协作的设计选型，其影响也会变得愈发关键。

人工智能放大基础架构的价值

当人工智能生成证明时，它会在目标系统的约束框架内运行。如果该系统具备表达力强的类型系统、强大的自动化功能和易读的符号体系，人工智能就能充分利用这些优势。就连错误提示的设计也至关重要：结构化、可操作的诊断信息能帮助人工智能高效修正错误，这与优质的错误提示对人类用户的帮助如出一辙。系统的表示形式决定了人工智能能否简洁地表达数学思想，而当我们的目标是将形式化证明拓展至整个数学领域、而非局限于某一本教科书时，简洁性的重要性不言而喻。

不妨这样理解：计算器的出现并未让数学变得无足轻重，它帮我们省去了繁琐的算术运算，让我们得以专注于真正的问题本身。但计算器的实用价值，完全取决于你所采用的数学框架——表示形式至关重要。

这一道理同样适用于人工智能与证明辅助工具的关系。若语言模型基于的系统具备依赖类型、类型类和设计良好的策略语言，它就能在恰当的抽象层级上表达数学思想。由此生成的证明更简短、结构更清晰，人工智能也能在更高的抽象层面开展工作。这是一种会不断叠加的优势。

可扩展性是真正的试金石

将拓扑学的一个章节进行形式化，已是一项令人赞叹的成果。但构建一个包含数十万条定理、且能长期维护的库，则是全然不同的挑战。这本质上是一个工程问题，而工程问题的解决效果，对设计选型的细节高度敏感。

简洁、结构良好的证明，是训练人工智能的优质数据；基于这些数据训练出的人工智能，又能生成更出色的证明；优质的证明反过来会提升库的实用性，进而吸引更多用户和贡献者。这是一个良性循环的飞轮，而证明辅助工具正是驱动飞轮转动的核心。越来越多的证据印证了这一点：谷歌深度思维（Google DeepMind）研发的强化学习系统AlphaProof，在2024年国际数学奥林匹克竞赛中斩获银牌，其底层正是基于一款拥有庞大且结构良好的库的证明辅助工具。正如谷歌深度思维的普什米特·科利（Pushmeet Kohli）所指出的，该系统的“可扩展性与验证能力”是取得突破的关键支撑。无独有偶，Harmonic公司（https://harmonic.fun ）研发的Aristotle系统，在2025年国际数学奥林匹克竞赛中达到金牌水准，同样基于这一技术基础；字节跳动的SEED Prover系统也在该赛事中获得银牌，底层框架亦别无二致。三支独立的团队，在最高水平的赛事中攻克同一难题，却不约而同地选择了具备表达力强的类型系统、庞大的库和可编程生态的证明辅助工具。不止这三家：Axiom Math（https://axiommath.ai ）、Math Inc（https://www.math.inc ）、Logical Intelligence（https://logicalintelligence.com ）等公司，也都在同一技术基础上开展研发。可见，底层工具的选择，是它们取得成功的关键因素，绝非偶然。

快速的证明校验速度也同样重要。当人工智能在反馈循环中探索数千种证明方案时，内核的运算速度会直接决定单位时间内人工智能的学习效率。这是一个现实存在的工程约束，证明辅助工具的研发者应当重视这一点。但仅有校验速度是远远不够的：一个运算速度快、却缺乏自动化功能和高效类型系统的内核，只能快速校验冗长繁琐的证明；而设计精良的系统生成的证明足够简洁，校验速度往往不会成为瓶颈。这两方面的优化是相辅相成的。

正是强大的自动化能力、表达力强的类型系统和清晰的定义归约机制，才让简洁的证明成为可能。它们是支撑人类与人工智能在恰当抽象层级开展工作的基础设施。

从理论走向实践

理论上，任何数学内容都可以在集合论或其他具备足够表达力的基础框架中实现形式化。这一点毋庸置疑，就像任何程序都能在图灵机上运行一样。

但从“理论上可形式化”到“实践中可落地”的鸿沟，恰恰是证明辅助工具设计需要攻克的核心问题。依赖类型让抽象代数、范畴论和现代代数几何的形式化成为现实，避免了陷入繁琐的编码冗余；类型类则让庞大的数学库具备可导航性和可组合性。证明辅助工具绝非仅仅是一个校验证明的内核，它是一整套完整的环境，决定了大规模场景下哪些数学内容的表达和维护具备实际可行性。

易读的规范说明：人类的信任契约

证明辅助工具能保证证明的正确性，但正确性本身还不够。必须有人去阅读定理的表述，并确认其准确捕捉了我们想要表达的数学思想。这是一份无论自动化程度多高都无法规避的人类契约。

能够编写让数学家可以审阅和理解的定义与定理表述，是证明辅助工具的核心要求。这一点直接取决于类型系统的表达力和符号机制的设计质量。现代工具进一步强化了这一能力：集成开发环境（IDE）支持鼠标悬停查看术语类型、跳转至定义、交互式探索库内容，这些功能让那些不会亲自撰写证明，但能够阅读和验证表述的人，也能接触到形式化数学。学习阅读形式化规范说明，远比学习撰写它们容易，而优质的工具让阅读过程变得更加便捷。当定义清晰易懂、工具易用性高时，数学家就能直接参与到形式化库的使用和验证中；反之，若定义被冗余的编码所掩盖，无论验证了多少定理，非形式化数学与形式化数学之间的鸿沟都将始终存在。

当人工智能负责生成证明时，这一点就更为关键。如果一个定理的形式化表述你完全无法解读，那么即便它的证明经过了验证，对你而言也毫无价值。你需要信任的，不仅是证明本身，还有规范说明。

有人可能会提出，人工智能可以在形式化表述与自然语言之间进行翻译，这样无论底层采用何种形式化框架，人类都能阅读通俗易懂的版本。但这种做法恰恰会在最需要保证正确性的环节，引入新的潜在错误源。形式化表述才是信任的基石。试想一个对抗性场景：有人声称证明了一项重要成果，此时你需要审阅的是真实的形式化表述，而非人工智能生成的摘要。易读的形式化规范说明并非人工智能可以替代的便利功能，而是信任的基础。

自动化作为“博弈步骤”

我认为有一种理解证明自动化的方式十分实用：证明器所具备的每一种策略或决策过程，都相当于博弈中的一步棋。如果一个系统只有基础的操作步骤（如应用引理、重写术语、展开定义），那么即便是常规的推理过程，也需要冗长的步骤序列才能完成；而具备强大自动化能力的系统，则能提供“一步到位”的操作，实现原本需要数百步才能完成的推理。

这对人工智能而言意义重大。用语言模型去完成数百步低层级的证明推导，就如同用语言模型去计算复杂的算术表达式——虽然理论上可以做到，但使用专用工具显然效率更高。强大的策略能让人工智能省去繁琐的常规工作，专注于数学上真正具有挑战性的决策：高层级的证明策略、引理的选择、关键的分支划分。工具应当负责其擅长的领域，人类和人工智能则聚焦于更核心的创造性工作。

正因如此，投入研发证明自动化技术（决策过程、简化器、通用策略），对人类用户而言绝非只是提升使用体验的改进，它还能直接提升人工智能生成证明的质量与效率。你为系统添加的每一种强大策略，都是人工智能可以利用的新能力。

理想的自动化工具应当兼具强大性与可控性。能一步完成目标证明的策略固然有价值，但更具价值的是那些可以交互式运行的策略，让人工智能能够逐步指导决策过程。这赋予了人工智能选择权：当简单操作足够时，可将策略作为单一的强力步骤使用；当问题复杂时，则可采取更精细的控制方式。不透明的自动化工具或许有用，但透明且可操控的自动化工具，才能带来革命性的改变。

可编程的生态系统

一款同时兼具编程语言属性的证明辅助工具，其叠加优势往往容易被低估。当策略、自动化组件、元程序和经过验证的代码都采用同一种语言编写时，所有模块都会相互赋能、形成合力。任何人（包括人工智能）都能编写新的自动化组件，无需切换开发环境或编程语言。“使用系统”与“扩展系统”之间的界限将不复存在。

这一点对人工智能的集成尤为重要。当人工智能不仅能撰写证明，还能编写新的策略、构建定制化决策过程、拓展系统功能时，就会形成一个正向反馈循环：系统越完善，越能助力人工智能；人工智能越强大，越能反过来优化系统。

展望未来

下一代顶尖的证明辅助工具，很可能会在人工智能的大规模协助下构建。在Lean FRO（https://lean-lang.org ）团队，我们早已将人工智能纳入开发流程。它带来了颠覆性的改变，如今我们已经无法想象脱离人工智能去开发Lean系统。在我们的代码仓库中，随处可见由人工智能参与撰写的提交记录。这一趋势只会愈演愈烈：人工智能将协助我们进行系统设计、生成核心库、编写自动化组件，并测试系统的人机交互体验。但评判一款证明辅助工具优劣的标准从未改变——它仍需具备表达力强的类型系统、易读的规范说明、强大的自动化能力、可编程的生态系统、优质的工具链和卓越的可扩展性。人工智能改变的是我们构建证明辅助工具的方式，而非衡量其优劣的核心标准。

当下已有的各类系统、它们的库、设计决策，以及在实践中积累的成败经验，都将成为构建下一代系统的训练数据和设计蓝本。过往的努力绝非徒劳，而是奠定未来发展的坚实基础。

没有任何技术能够永远存在，这恰恰是进步的标志，而非失败。我们的目标并非构建一个能永久存续的系统，而是推动形式化数学的发展进程，让形式化数学、经过验证的软硬件变得切实可行、易于获取且具备实用价值，让下一代技术能站在更高的起点上出发。如果未来出现了真正更优越的系统，那就意味着我们的使命已经达成。

我所关心的是，这一发展进程始终由真正的技术进步驱动。在人工智能时代，评判优质证明辅助工具的标准已然清晰，且其重要性正前所未有地凸显。

参考资料

https://leodemoura.github.io/blog/2026/02/18/proof-assistants-in-the-age-of-ai.html