数学证明的AI革命：一场关于严谨性的内战

伦敦帝国理工学院的数学家凯文·巴扎德正在教计算机证明费马大定理——一个1998年就已经有公认证明的古老问题。这不是为了解题本身，而是为了验证一种全新的工作方式：让机器彻底理解数学。

形式化：把直觉翻译成代码

传统数学证明依赖纸笔、黑板和直觉。数学家写下"显然成立"的步骤，同行凭借专业训练心领神会。这种模糊地带正是人类智慧的体现，也是机器长期无法触及的禁区。

形式化（formalization）要求把每个定义、每个定理都翻译成计算机代码，让专用程序验证每一步。约翰霍普金斯大学的数学家埃米莉·里尔说，这"本质上要求证明作者比平常严谨得多"——计算机不会帮你填坑，你得自己把每个缝隙焊死。

巴扎德的目标更宏大：建造一个包含全部数学的数字图书馆，让计算机成为数学家的真正助手。费马大定理的证明横跨多个数学领域，填满约130页两篇论文，正是理想的试金石。

正方：AI让不可能成为可能

大语言模型的爆发改变了游戏规则。科技公司正带头推动"自动形式化"（autoformalization）——把自然语言证明直接转换成机器可验证的代码。

理论上，这类系统最终能做到人类无法做到的事：检查超大规模证明中的逻辑漏洞，发现跨领域的隐藏联系，甚至提出人类想不到的证明路径。美国国防部高级研究计划局（DARPA）的数学家帕特里克·沙夫托说："我们正处于变革的临界点。"

他预测："数学现在基本上还是在黑板上进行，和100年前一样。但我认为五年内，很可能每个年轻数学家……"——话没说完，但指向已经很明确。

对支持者而言，这不是威胁而是解放。当机器接管验证的脏活累活，人类可以专注于更本质的创造。

反方：精确性会杀死数学的灵魂

反对者看到的是另一幅图景。数学的进展从来不是靠绝对严谨驱动，而是靠直觉、跳跃和"显然成立"的默契。把证明写成代码，就像要求诗人用语法规则解释为什么这句诗动人。

更深层的焦虑关乎权力结构。如果形式化成为标准，谁来定义"足够严谨"？大型科技公司的技术栈会不会成为数学研究的准入门槛？年轻数学家是解放了，还是被新的技术官僚体系绑架了？

一个原本纯粹的哲学问题——数学证明的最大精确度可能达到什么程度——现在变成了存在主义危机：对精确性的追求会不会颠覆整个领域？

判断：工具不会取代判断，但会重塑判断的成本

这场辩论的核心被误置了。真正的问题不是"机器会不会取代数学家"，而是"验证的成本结构正在发生根本性变化"。

历史上，数学共同体的信任机制建立在声誉和同行评审上。一个证明被接受，不是因为每个步骤都被机械验证，而是因为足够多可信的人说"我检查过了"。这种机制有漏洞——错误证明可以潜伏多年——但效率极高。

形式化+AI提供的是另一种选择：用算力换信任。当验证成本下降到某个阈值，数学研究的组织方式必然调整。某些领域（如需要大规模计算的证明）会率先迁移，另一些领域（如依赖几何直觉的拓扑学）可能长期保持传统。

巴扎德的项目揭示了一个更务实的真相：形式化不是要把所有数学塞进计算机，而是要建立一个"可验证层"——当你需要绝对确定时，有一个选项。

最可能的结果是分层。基础架构层高度形式化，应用层保持灵活。就像软件工程：底层库经过严格测试，上层业务代码快速迭代。数学家会学会在两种模式间切换，根据问题性质选择工具。

沙夫托的五年预测可能过于乐观，但方向没错。变化不会来自"AI证明定理"的轰动新闻，而来自年轻研究者默默养成的习惯：先形式化验证核心引理，再展开直觉推导。

费马大定理的证明花了358年才找到，又花了130页纸才写完。巴扎德教计算机理解它，不是为了更快解题，而是为了证明一件事：最艰深的数学直觉，终将被翻译成机器可检验的语言。这个过程本身，就是数学的又一次自我更新。

至于那些担心灵魂丢失的人——数学史上每一次工具革命都伴随类似哀鸣。坐标系杀死了几何的纯粹性，集合论颠覆了分析的直觉，计算机辅助证明曾被视为异端。结果数学不仅存活，而且膨胀。

严谨性不会杀死数学，它只是数学的另一种形态。真正的问题是：你愿意为确定性支付多少成本？