在数学中，严谨性至关重要。但数字化证明是否矫枉过正了？

2026年初，一个消息在数学圈悄然流传：伦敦帝国理工学院教授凯文·巴扎德，正在用一套计算机程序重写人类历史上最著名的数学证明之一，费马大定理。这不是什么学术噱头，而是一场正在改变数学本身面貌的运动的缩影。

这套程序叫Lean，是一种"证明助手"。你往里输入一个数学证明，它逐行检查每一步推导。哪怕有一个细节没说清楚、逻辑没闭合，程序就判你出局。目前，Lean的数学库已收录超过12万个定义、验证了逾25万条定理，背后有超过1000万美元的资金支持，主要来自亿万富翁金融家亚历克斯·格尔科。

支持者的理由非常有力：数学文献里的错误比人们愿意承认的多得多。

欧几里得的《几何原本》标志着西方数学形式化进程的首次重大尝试。它确立了一种演绎推理的证明方法，至今仍在使用。上图为该著作1482年首版印刷本的内页。福尔杰莎士比亚图书馆/知识共享署名

严谨，从来都不是免费的

数学追求严谨的历史，本身就是一部充满争议的戏剧。

19世纪初，柯西和魏尔斯特拉斯重新定义了极限概念，把微积分从一套"用起来管用但说不清楚"的工具，改造成逻辑严密的分析学体系。这是数学史上的重大飞跃，却也让一些同时代的科学家感到窒息。物理学家赫维赛德在1899年抱怨，"冷漠的严苛主义者"浇灭了他的热情。

阿基米德在其著作《论圆锥体和球体》（此处为 1897 年译本）中提出了一些思想，这些思想在几千年后的微积分发展中发挥了关键作用。摘自TL Heath编辑的《阿基米德的著作》。剑桥大学出版社，1897年/公共领域

再往后，20世纪30年代兴起的布尔巴基学派走得更远。这个法国数学家秘密团体把抽象和逻辑推到了极致，用最严密的形式语言重写了几乎整个数学体系。效果是惊人的：数学变得更可靠，也更内在统一。代价同样是惊人的：具体、图形化的数学分支，比如组合数学和图论，被这套风格边缘化了几十年，只能在匈牙利等布尔巴基影响力较弱的地方偷偷发芽。

南加州大学数学家阿拉文德·阿索克用一句话总结这段历史："我不希望任何一种数学模式占据主导地位，数学蕴含着丰富的文化历史，值得我们去传承。"

戈特弗里德·莱布尼茨（左）和艾萨克·牛顿在17世纪各自独立地发明了微积分。多年来，他们一直争论谁先提出了微积分的核心思想。克里斯托夫·伯恩哈德·弗兰克（左）；戈弗雷·内勒

这句话今天依然刺耳，因为Lean的推进方式，在某种程度上正在重演布尔巴基的逻辑。

一把双刃剑

Lean最令人信服的一次亮相，发生在2020年前后。数学家彼得·舒尔茨写出了一个关键定理的证明，但它极为复杂，连他自己都没法确认正确性。一个团队花数月时间将其用Lean形式化，不仅确认了证明无误，还在这个过程中找到了更简洁的表达，并深化了舒尔茨的原始构想。

19 世纪，奥古斯丁-路易·柯西（左）和卡尔·魏尔斯特拉斯重新定义了微积分中的关键概念，从而产生了现代分析学领域。史密森尼图书馆（左）；公共领域

陶哲轩也有过类似经历。他在用Lean形式化自己论文的过程中，发现了一个此前未察觉的小但重要的错误。这类故事，是Lean支持者最喜欢讲的案例：机器不只是验证工具，它逼着你把每一个隐含假设都摆到台面上，在这个过程中，你可能会看到自己从未意识到的东西。

尼古拉斯·布尔巴基

成立于 20 世纪 30 年代的秘密数学社团布尔巴基（Bourbaki）将严谨性、抽象性和逻辑性置于一切之上。其创始成员包括亨利·嘉当（站立者，最左侧）、安德烈·韦伊（站立者，右数第二个）和索莱姆·曼德尔布罗伊特（坐着，右侧）。巴扎德这样形容Lean的体验："它迫使你以正确的方式思考数学，它迫使你成为一名艺术家。"

然而，批评的声音同样清醒。用Lean形式化一个证明，通常需要几个月，有时超过一年。而数学界的现实是，同等时间投入，在传统研究方式下完全可以产出新的定理、新的联系、新的领域。

西蒙弗雷泽大学历史学家斯蒂芬妮·迪克说得直接：数学"并非一门固定、有限且形式化的学科"，它的规则本身也在不断演变。而Lean的库结构要求所有定义必须无缝衔接，一旦某个基础定义被更新，依赖它的大量证明可能随之失效，牵一发而动全身。

更深层的担忧在于：当一种工具成为标准，它就悄悄地定义了什么样的数学"值得被做"。

Lean与人工智能的结合，已经让这种担忧变得更加迫切。2026年1月，AI模型在一周内攻克了三道困扰数学界已久的埃尔德什问题，生成的证明经Lean形式化验证后被陶哲轩本人接受。这是一个令人震撼的信号：当AI开始大规模生产证明，Lean这样的验证工具将成为不可或缺的基础设施。但与此同时，如果AI和Lean共同构成新的数学生态，那些不容易被形式化的领域，那些依赖图形直觉、模糊类比或尚未命名的新思想的领域，会不会再度遭到系统性冷落？

数学家大卫·希尔伯特在1905年写过一句话，今天读来依然清醒："科学大厦的建造，并非先打好地基再往上盖，而是先找到舒适的空间四处走动，等出现迹象表明松动的地基无法支撑扩张时，才去支撑和加固它。"

这场围绕Lean的争论，本质上是在问同一个问题：我们现在是在加固地基，还是把地基变成了笼子？

信息来源：量子杂志