2023 年 11 月，菲尔兹奖得主陶哲轩（Terence Tao）和合作者 Timothy Gowers、Ben Green、Freddie Manners 共同宣布证明了多项式 Freiman–Ruzsa（PFR）猜想。这不只是一个数学定理的证明。
他们的证明是在 Lean 4 这个形式化证明系统中完成并验证的。在人类证明一个定理的同时，计算机验证了证明的每一步逻辑上正确、没有遗漏。这是近年来规模最大的"人机协作数学证明"之一。
2024 年，DeepMind 的 AlphaProof（配合几何专用系统 AlphaGeometry 2）在国际数学奥林匹克（IMO）2024 年的题目上正确解决了六道题中的四道，其中 AlphaProof 解出的题目以 Lean 4 形式写出并经形式化验证——这是首次有 AI 在 IMO 上达到"大致银牌"的表现。
这两件事标志着形式化验证正在从"需要极大人工投入"的专业工具，向"可以由 AI 辅助的"普通工程工具转变。
破除误解：形式化验证不只是"测试更多"
软件测试（单元测试、集成测试、模糊测试）可以发现 bug，但无法证明没有 bug——测试只覆盖特定的输入，你永远无法测试所有可能的情况。
形式化验证的目标是数学上的正确性证明：对程序或系统的所有可能输入和状态，证明它满足某个规约（specification）。不是"我们测了 1000 个情况，没发现问题"，而是"我们数学上证明了，对所有情况，它都满足规约"。
这不仅适用于软件：硬件芯片、通信协议、密码算法都可以形式化验证。Intel 的浮点运算单元曾因 bug（Pentium FDIV bug，1994）损失数亿美元，此后硬件验证成为工业实践。
现场：CompCert 与经过证明的编译器
计算机程序由编译器把人类可读的源代码翻译成机器指令。如果编译器本身有 bug，会引入人类没有写进源码的错误——这些错误很难检测，因为人类审查源码，机器运行机器码。
Xavier Leroy（INRIA）领导开发的 CompCert 是第一个在 Coq 证明系统中被完整形式化验证的优化 C 编译器。CompCert 的机器可读证明保证：编译前后的程序在语义上等价——源码做什么，机器码就做什么，没有编译器引入的语义错误。
CompCert（2009 年首次发表完整版）已被航空、汽车、核电等安全关键领域采用。它的证明约 10 万行 Coq、耗费约 6 个人年——证明了对一个复杂的实用系统，完整形式化验证是可行的。
这里有一个堪称"实证"的旁证：Yang 等人（PLDI 2011）用随机程序生成器 CSmith 去"轰炸"主流 C 编译器，在 GCC 中找出 79 个、在 LLVM 中找出 202 个能让编译器静默生成错误代码的 bug——而在 CompCert 被形式化验证的那部分，他们一个错误代码 bug 都没找到。换句话说，形式化验证不是纸上谈兵，它确实把一整类 bug 从根上消除了。值得精确指出的是：CompCert 早期发现的极少数缺陷，都落在没有被证明覆盖的边缘部分（如早期版本的源码解析前端）——这也点出了形式化验证的一条铁律：证明只对它所覆盖的范围负责，没纳入证明的代码（解析器、运行时、汇编器）仍可能出错。
Lean 4 与数学证明的新生态
Lean 4（Leonardo de Moura，2021 年发布）是近年最受关注的交互式定理证明器（Proof Assistant）。前几代系统（Lean 3、Coq、Isabelle/HOL）已经证明了大量重要数学定理（如四色定理、Kepler 猜想）。Lean 4 改进了系统设计，同时也是一门通用编程语言，降低了"证明代码和普通代码共存"的障碍。
Mathlib 是建立在 Lean 4 上的大型数学库，由全球数百名贡献者维护，包含数千个数学领域的形式化定义和定理。它是人机协作数学的基础设施，也使 AI 系统可以从大量已有的形式化证明中学习。
陶哲轩等人的 PFR 猜想证明，正是在 Lean 4 + Mathlib 的基础上完成的。
AI 辅助形式化证明：两种路线
路线一：用 LLM 写证明代码
大语言模型（如 GPT-4、Claude）被用来直接生成 Lean 4、Coq 或 Isabelle 的证明代码。优点：LLM 可以从大量已有证明中学习模式。缺点：LLM 会产生幻觉，生成语法上合法但逻辑错误的证明片段。
Lean-GPT 系列工作（2023-2025）：多个团队把 LLM 与证明搜索结合，LLM 提出候选证明步骤，系统验证后接受或拒绝，构成反馈循环。
路线二：专用的数学推理系统
AlphaProof（DeepMind，2024）：把强化学习训练的推理模型与 Lean 4 形式验证结合。模型生成候选证明步骤，Lean 4 验证；验证通过的证明为模型提供正向奖励，构成强化学习信号。这与 LLM 不同：每一步都有数学真实性保证，不依赖模型的"直觉"。
IMO 2024 测试：六道题，DeepMind 系统合计解出 4 道——AlphaProof 解决了两道代数题与一道数论题（含全场最难、仅 5 名选手做出的一题），并自动生成 Lean 4 证明；唯一的几何题（P4）则由专用系统 AlphaGeometry 2 解决。剩余两道组合题因形式化困难、搜索空间爆炸而未能攻克。系统总分 28/42，达到银牌水平（距金牌门槛仅差 1 分）。
2025 年，ACM SIGPLAN 编程语言软件奖颁给了 Gabriel Ebner、Soonho Kong、Leonardo de Moura 和 Sebastian Ullrich，表彰 Lean 对数学、硬件/软件验证和 AI 的"重大影响"。
程序合成：自动写正确的代码
程序合成（Program Synthesis）的目标比验证更进一步：给定规约，自动生成满足规约的程序。
经典路线：Sketch（Armando Solar-Lezama, 2006）让程序员写出程序的"草图"（有空洞的程序），自动搜索填充空洞的方案，使程序满足给定测试或形式规约。
现代路线：
- FlashFill（Gulwani, 2011）：Excel 中"从示例自动推导数据变换程序"的功能，是程序合成第一个大规模商业成功案例。
- LLM 生成 + 形式验证：让 LLM 生成候选代码，用形式验证（或测试）过滤，只保留正确的。2024-2025 年涌现了多个将 LLM 和 Lean/Coq 结合的程序合成框架。
代价与争议
可扩展性的根本挑战：形式化验证的成本极高。经验表明，对一个复杂的工业系统写出完整的形式化证明，所需工作量通常是原始开发工作量的 5-20 倍。这在学术研究和安全关键系统（核电、航空）可接受，在普通软件开发中极难推广。
规约问题：形式化验证保证程序满足规约，但规约本身可能是错的——描述了错误的需求，或遗漏了重要情况。"规约错误"不能被形式化验证发现。正确写出规约有时比写程序本身更难。
AI 生成证明的可信度：AlphaProof 的证明由 Lean 4 独立验证，这部分是可信的。但证明策略的选择、证明思路的来源，对人类来说仍是不透明的——这是一个"正确但难以理解"的证明，在数学文化中的意义有争议。
工具生态碎片化：Lean、Coq、Isabelle、HOL4 各有优点，社区分散，定理很少能跨系统迁移。统一形式化数学基础设施是长期难题。
未知的边界
- AI 辅助证明能否扩展到当前人类尚未解决的数学猜想（如黎曼猜想、P vs NP）？
- 形式化验证是否能在经济上可行地推广到普通软件开发，还是永远只是安全关键系统的专利？
- 如果 AI 可以自动发现并证明数学定理，"数学家"这一职业的角色会如何演变？
- LLM 辅助的程序合成，是否会改变软件正确性的标准——从"测试通过"到"形式化验证通过"？
- AlphaProof 类的系统目前只在有精确形式化表述的数学问题上有效（如 IMO 竞赛题）。对于数学研究中典型的"模糊的直觉驱动的探索"，AI 能否胜任仍完全未知。
- 如何在 Lean / Coq 等不同证明系统之间迁移已有的形式化知识，是基础设施层面的长期挑战，目前各生态相互割裂。
- 程序合成的"意图鸿沟"（intent gap）：从用户意图到精确规约，本身就需要人类介入。如何让非专家用户用自然语言描述需求，自动转化为可验证的形式规约，是连接 LLM 能力和形式化方法的关键未解问题。
- 超大规模软件系统（如 Linux 内核、浏览器）的完整形式化验证，在工程量上是否存在根本性障碍，还是只是时间和工具问题？最经典的全功能形式化验证项目（seL4 微内核，约 8,700 行 C 代码、用 Isabelle/HOL 证明，Klein 等, 2009）相比工业级系统仍小得多。
- AI 辅助程序合成能否可靠地生成安全关键代码（航空、医疗设备），还是幻觉问题始终让其无法通过安全认证标准？
- 形式化验证在硬件设计（RTL 验证）中已较为成熟（Intel、AMD、Arm 都使用等价性检查和模型检查工具），但软件侧尤其是并发软件的全面验证，仍是工业上的未解挑战。
跨域连接
- 类型系统：证明助手的地基是类型即命题：一个类型是一条断言，一个通过检查的项就是它的证明。依赖类型让类型可以引用值，规约因而能直接写进类型签名，"编译通过"与"满足规约"合二为一。代价是类型检查的代价随表达力上升，工程上总要在某处停手。
- AI 与形式化证明：这条路线的关键结构是把生成与检查分开：模型可以不可靠地提议，内核必须可靠地判定。幻觉因此被挡在验证器之外，正确性不依赖模型的自信。适用边界也随之明确——只有能被形式化陈述的问题才享有这层保护，模糊的、直觉驱动的探索不在其中。
- 哥德尔不完备定理：把全部数学机械化的雄心早已被证明有界，而这条界与今天的工程约束是两回事。真正每天咬人的是另一条更朴素的规则：证明只对它覆盖的范围负责——未纳入证明的解析器、运行时与汇编阶段照样会出错，实际缺陷也确实集中在那里。
- 法治：验证保证程序满足规约，但规约表达的是意图，而意图与条文之间必有缝隙。这与法条无法穷尽立法目的是同一类问题：两边都得靠一个形式系统之外的程序——人工评审或司法解释——补上系统内无法自证的那一层。规约写错，验证发现不了。
- 零知识证明：验证电路的缺陷是静默的：它不报错，只是让伪造的证明被接受。当一次失败的代价远高于验证成本时，形式化才在经济上划算——这正是它先在密码电路、编译器与操作系统内核落地，而不在普通应用里普及的原因。
参考文献
- Leroy, X. Formal Verification of a Realistic Compiler. CACM 52(7), 2009. （CompCert 的概述）
- de Moura, L. & Ullrich, S. The Lean 4 Theorem Prover and Programming Language. CADE 2021.
- AlphaProof 团队. AI Achieves Silver-Medal Standard Solving International Mathematical Olympiad Problems. Google DeepMind 博客, 2024. （deepmind.google）
- Gulwani, S. Automating String Processing in Spreadsheets Using Input-Output Examples. POPL 2011. （FlashFill 的学术论文）
- Yang, X., Chen, Y., Eide, E. & Regehr, J. Finding and Understanding Bugs in C Compilers. PLDI 2011. （CSmith：在 GCC/LLVM 中找到大量 bug，CompCert 验证部分无错码 bug）
- Klein, G. et al. seL4: Formal Verification of an OS Kernel. SOSP 2009. （首个全功能验证的操作系统微内核）
- Avigad, J. Mathematics and the Formal Turn. 2023. arXiv:2311.00012.