如何形式化整个数学？一场正在发生的范式变革

数学，这门最讲究严谨的学科，正在经历一场自我验证的技术革命。它的目标是：把人类数千年积累的全部数学知识，翻译成计算机可以逐字核对的代码。

从个别突破到全学科野心

在相当长的一段时间里，形式化数学（Formalized Mathematics）都是零散工程。Lean 等证明助手虽然在个别定理上有所建树，但远谈不上覆盖整个学科。如今，这个领域正在从"证明一个难题"转向"重写整个数学体系"。

Hacker News 上围绕"How to Formalize All of Mathematics"的讨论引发了广泛关注。这不再是单纯的技术路线之争，而是一个根本性问题：数学的终极形态，究竟是人类纸笔上的推理，还是机器可验证的形式化证明？

形式化数学指的是把数学定义、定理陈述与证明，改写成计算机可以逐步检查的形式语言。它不同于数值计算或符号运算，因为其核心不在于快速算出结果，而在于确认“每一步推理是否合法”。

证明助手（proof assistant，也称交互式定理证明器）是支撑形式化数学的软件系统。常见代表包括 Lean、Coq、Isabelle/HOL、Agda 等。使用者需要用这些系统规定的语言写下定义、引理和证明脚本，系统则基于严格的类型检查或证明检查机制，判断证明是否成立。

因此，形式化数学并不是用计算机“更聪明地猜出定理”，而是把数学证明变成一种可审计、可复现的工程产物。

为什么现在要形式化数学？

传统数学中的证明，依赖同行评审和人类直觉。这种方式虽然有效，却隐藏着风险。一个被长期接受的证明，可能在几十年后被发现存在漏洞。四色定理、开普勒猜想等案例都曾经历从"公认"到"争议"再到"机器验证"的曲折过程。

形式化的核心承诺是：一个证明一旦被形式化，就不再需要争论。 计算机逐步检查每一步推理，逻辑漏洞无处藏身。对于数学而言，这意味着可靠性达到前所未有的高度。

更重要的是，AI 的介入改变了游戏规则。大型语言模型可以辅助生成证明草稿，而形式化工具则充当最终的裁判。这种"AI 生成 + 形式化验证"的组合，正在大幅降低形式化的边际成本。

AI 生成 + 形式化验证之所以受到重视，是因为大语言模型擅长处理自然语言和代码草稿，但会产生看似合理、实则错误的推理。形式化验证则相反：它不依赖模型的自信程度，只接受能通过证明助手逐行检查的结果。

这种组合的潜力在于分工：模型负责提出候选证明、补全繁琐步骤、把自然语言转成形式语言；证明助手负责判定对错；人类数学家则负责选择问题、提供高层直觉和修正方向。它并不能替代数学判断，但可以显著降低形式化的时间成本，让更多定理进入机器可验证的轨道。

数学形式化面临的核心难题

知识覆盖的规模问题

已有数学文献浩如烟海。从欧几里得的《几何原本》到现代代数几何，尚未形式化的定理数量惊人。即便 Gödel 不完备性定理这类经典结果早已被形式化，绝大多数当代研究论文仍停留在纸笔阶段。

形式化与数学直觉的鸿沟

数学家在思考时，依赖大量未经形式化的直觉和类比。形式化要求把这些隐含假设全部显式化，这既是挑战，也是价值所在——它强迫我们审视那些"显然"的步骤是否真的成立。

数学论文中的“显然”“同理”“不失一般性”等表述，往往压缩了大量背景知识。人类读者能靠经验和语境补全，但形式化系统不会默认这些隐含前提。

因此，形式化过程常被比作“把冰山搬到水面上”：数学家只写出冰山一角，形式化则要求把水下部分也逐一定义、证明和连接。这会暴露原本被忽略的边界条件、特殊情形和依赖关系。

这一过程的价值不只是让机器信服，也会反过来帮助人类发现证明中的真正结构。许多形式化项目都会在此过程中找到原论文里模糊甚至错误的地方。

社区协作与标准统一

不同项目使用不同的库、不同的记号系统，如何协同工作？这不仅是技术问题，更是文化问题。数学界需要像开源社区那样，建立共享的基础设施和协作规范。

在形式化数学中，库（library）指已经形式化的定义、定理和证明代码的集合。例如 Lean 的 mathlib 就是一个大型协作库，目标是覆盖现代数学的广泛基础。不同证明助手之间的库通常不能直接通用，因为底层逻辑、类型系统和语法不同。

标准统一的难点不仅是接口问题，还涉及数学表达风格：同一个概念可能有多种等价定义，选择哪一种会影响后续证明的难易。因而社区需要建立命名规范、依赖管理、版本控制和贡献审查机制。这类似开源软件工程，但对象是数学知识本身。

AI 时代的加速器效应

据近期讨论，AI 工具正在成为形式化数学的关键推手。一方面，模型可以自动填补形式化证明中的琐碎步骤；另一方面，模型也能从自然语言陈述中提取出可形式化的定义。

这种分工正在成型：

• 人类数学家用自然语言提出猜想和证明思路
• AI 负责将其转化为形式化代码初稿
• 证明助手验证每一步逻辑
• 人类复核结果并修正方向

这个流程的成熟，可能让形式化的速度提升数个数量级。

对数学未来的深层影响

如果整个数学最终被形式化，后果远超"证明更可靠"这一点。

数学知识将成为可计算、可查询、可自动组合的资源。一个数学家想要使用某个定理，只需调用对应的形式化条目，机器会处理所有前提条件。数学教育、数学研究、甚至数学发现的模式，都将被重塑。

当然，这条路不会一蹴而就。它需要几代人的努力，需要工具链的持续完善，也需要数学文化自身的调整。但方向已经清晰：数学正在从"人类可读"走向"机器可验证"，而这个转变才刚刚开始。

形式化数学的意义不在于质疑数学家的能力，而在于为数学建造一座永不会坍缩的框架。