数学中，严谨至关重要，但数字化证明是否过犹不及？——译自量子杂志Quanta Magazine|代数|微积分|数字化证明|数学家|牛顿|莱布尼茨|量子杂志

★置顶zzllrr小乐公众号（主页右上角）数学科普不迷路！

数学家们正致力于用Lean计算机程序将所有数学内容形式化，而数学追求严谨的历程漫长且曲折，这段历史值得他们借鉴。

图源：Kristina Armitage / Quanta Magazine

作者：Leila Sloman（莱拉·斯洛曼，量子杂志特约通讯员）2026-3-25

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

在古希腊，欧几里得证明了只要认同一小部分基本原理（即公理），人们就能通过演绎推理发现各类全新的数学真理。但数学家们所称的这些早期证明，即便依据逻辑法则推导而来，有时也暗藏未阐明的假设，或是依赖易产生误导的直觉。在这类情况下，证明中细微的漏洞可能被忽略，人们无法绝对确信其正确性。

过去几个世纪里，数学家们一直试图填补这些漏洞。到20世纪初，他们确定了想要使用的公理，还引入了不同的逻辑体系和标准，力求让论证进一步“形式化”——确保若将证明中的每一步推导都清晰呈现，无论过程多么冗长复杂，结论都必然成立。

这场形式化的努力不仅建立了信任，更带来了诸多意外收获。推动数学形式化的过程，让数学家们发现了不同数学领域间全新的关联，将数学研究引向了意想不到的新方向。明尼苏达州麦卡利斯特学院的戴维·布雷苏德（David Bressoud）表示，这一过程让我们明白：“你往往不知道自己还有哪些未知，也因此要保持谦逊。”

但数学领域的重大突破，必然需要大胆的想法。这些想法往往源于实验与直觉——探索全新的数学领域，验证新颖的数学理论，即便你无法证明探索过程中的每一步，都能从逻辑上承接上一步。这种研究数学的方式形式性较弱，初期也容易出现谬误。

在描绘全新数学图景所需的创造力，与确保这些图景真实成立所需的严谨性之间，找到卓有成效的平衡并非易事。有时，形式化会打破这种平衡。在一些数学家眼中代表着对更高确定性的追求，在另一些人看来，或许只是繁琐的钻牛角尖，或是阻碍发展的壁垒。

欧几里得的《几何原本》，是西方数学史上首次大规模的形式化尝试。它确立的命题证明演绎法，至今仍在沿用。上图为1482年问世的《几何原本》首个印刷版本内页。

图源：福尔杰莎士比亚图书馆/知识共享署名-相同方式共享4.0协议

如今，数学家们正开展迄今最宏大的形式化项目：试图用一种名为Lean的计算机语言重写所有数学内容，再由程序自动验证这些证明。用Lean撰写证明需要投入大量的时间和精力，但截至目前，该程序已验证了超过26万个定理，有望为数学搭建起人类所能想象的最坚实的基础。

与以往的数学形式化尝试一样，Lean也引发了数学家们复杂的情绪。一些数学家期待将繁琐的验证工作交由计算机完成，将Lean视为改变数学研究方式的潜在革命性工具；另一些则认为，时间和资源应用在其他更有价值的研究上，更有甚者担心，以Lean为核心的研究方式，会扭曲数学的真正价值。一场关于“如何平衡发现数学新关联所需的创造力，与确保每一步逻辑都无懈可击所需的严谨性”的讨论，正在全球各数学系的走廊里展开。

设定边界

数学追求严谨的历程中，一个重要里程碑的出现，源于一项旷世数学成就背后隐藏的问题。

17世纪末，艾萨克·牛顿和戈特弗里德·莱布尼茨各自独立创立了微积分——这一用于研究函数在某一点变化速率的方法。但从非形式化的角度来看，微积分的雏形早在数百年前就已出现。事实上，公元前3世纪，阿基米德的研究就已具备微积分的雏形。为计算圆的面积，他先研究了由直线构成的图形（即多边形）的面积，通过不断增加多边形的边数，去逼近一个极限值：圆的面积。牛顿和莱布尼茨采用了类似的思路，借助极限来阐释变化的概念。

在这本 1897 年译本的著作《论劈锥曲面体与椭球体》 On Conoids and Spheroids 中，阿基米德（Archimedes）提出的诸多思想，在千年之后的微积分发展进程中发挥了关键作用。

内容出自 T・L・希思（T.L. Heath）校订的《阿基米德著作集》，剑桥大学出版社 1897 年版，公有领域。

微积分一经诞生，便迅速在数学和物理学领域发挥重要作用，但以现代标准来看，它在当时并不具备形式化的特征：牛顿和莱布尼茨的论文回避了一些模糊不清的问题。微积分以无穷和无穷小量（即微元）为核心概念，可两人仅用模糊的几何语言对其进行定义；若公式使用不当，便会得出诸如除以零这类毫无意义的计算结果。

在之后的150年里，这一问题并未引发任何麻烦，科学家们早已摸索出微积分的有效适用场景。但到了19世纪初，数学家们开始遇到一些违背直觉的现象——比如无穷级数、形态怪异的锯齿曲线等。

这一时期，艺术和科学领域也正经历大范围的质疑与反思，哲学家、画家、作家和研究人员纷纷开始探寻认知的边界。哥伦比亚大学的科学史学家阿尔玛·施泰因加特（Alma Steingart）表示：“直觉开始受到质疑，人们意识到，直觉可能会引向错误的方向。”

戈特弗里德・莱布尼茨（Gottfried Leibniz，上）与艾萨克・牛顿（Isaac Newton，下）于 17 世纪各自独立创立了微积分。多年来，两人就微积分核心思想的首创权争执不休。

肖像作者：克里斯托弗・伯恩哈德・弗兰克 Christoph Bernhard Francke，上图；戈弗雷・内勒 Godfrey Kneller，下图

尼尔斯·阿贝尔（Niels Abel）、奥古斯丁-路易·柯西（Augustin-Louis Cauchy）、卡尔·魏尔斯特拉斯（Karl Weierstrass）等著名数学家意识到，要理解研究中出现的这些奇异级数和曲线，必须回归最基础的定义：什么是函数？函数的连续性意味着什么？无穷多个对象相加的本质是什么？

他们为这些问题给出了形式化的定义（例如，魏尔斯特拉斯提出的极限精确定义，至今仍被学生沿用）。这些新定义让数学家们得以以前所未有的深度和严谨性研究函数，最终催生了分析学这一数学分支。

如今，分析学已是数学领域最重要的分支之一，数学家们借助它研究从流体流动、电流传导，到遥远恒星的化学成分等各类问题，且它与数论、几何学等历史更悠久的数学分支，以及几乎所有其他数学领域都有着紧密关联。而微积分的形式化，也推动了集合论的诞生——这一理论确立了现代数学的底层规则，如今集合论本身也成为了一个活跃的研究领域。

19 世纪，奥古斯丁 - 路易・柯西（Augustin-Louis Cauchy，上）与卡尔・魏尔斯特拉斯（Karl Weierstrass，下）重新定义了微积分中的核心概念，由此催生了现代分析学这一数学分支。

图源：史密森尼学会图书馆 The Smithsonian Libraries，左图；公有领域，右图

即便如此，当时也有一些研究者对这股形式化浪潮心存顾虑。1899年，物理学家奥利弗·亥维赛（Oliver Heaviside）写道：“当严谨派的冷水浇灭了热情，便再难让人提起兴致。”

科学史学家耶斯佩尔·吕岑（Jesper Lützen）在回顾这一时期时指出 https://www.ams.org/publications/authors/books/postpub/hmath-24 ：“分析学在收获严谨性和一般性的同时，失去了简洁与优雅，也与直觉渐行渐远。许多数学家对这一趋势感到惋惜，却又无力改变。”

关键的是，严谨派数学家与反对者最终达成了妥协：数学家们继续沿用柯西和魏尔斯特拉斯提出的严谨定义，同时也构建了新的框架，让亥维赛等科学家能更自由地对无穷和无穷小量进行计算。

伦敦帝国理工学院的凯文·巴扎德说：“形式化会迫使你用正确的方式思考数学，也会迫使你成为一名‘艺术家’。”

换言之，形式化并非他们的唯一目标。事实上，这段历史的关键，在于形式化背后的初衷：其研究范围相对狭窄，魏尔斯特拉斯及其同僚当时正研究与函数行为相关的特定问题，形式化只是他们解决这些问题的手段。而分析学、集合论及其他形式化体系的发展，都是在此基础上自然展开的。

大数学家戴维·希尔伯特在1905年写道 https://www.leocorry.com/_files/ugd/e6fef7_dbe9131a54ed48c996cd517588422cdd.pdf ：“科学大厦的构建，并非像建造房屋那样，先牢牢打下地基，再着手建造、扩建房间；相反，科学家应先找到可以自由探索的‘舒适空间’，只有当各处出现松动的地基无法支撑房间扩建的迹象时，再去加固地基。”

他接着说：“这并非缺陷，而是科学发展正确且健康的路径。”

毕竟，当形式化的目标超出了加固松动地基的范畴，其产生的影响也会截然不同。

刻板的学术体系

对清晰性和严谨性的追求，也可能走向极端。

数学界有一个著名（或说声名狼藉，取决于不同人的看法）的学术流派，由一个名为布尔巴基的数学家秘密团体提出，便是典型的例子。

20世纪30年代中期，法国的数学研究已衰落数十年：第一次世界大战让法国失去了一代极具潜力的学生和研究者；各大学的数学教学缺乏协调、体系零散，使用的教材也早已过时。于是，几位年轻的数学家联合起来，创立了布尔巴基学派。他们最初的目标很朴素：编写一套全新、更系统的教材，让法国的数学课程体系跟上现代步伐。但很快，他们的野心不断膨胀。如今，成员身份仍处于保密状态的布尔巴基学派，已出版了40多卷著作，涵盖了数学领域的所有分支。

1930年代创立的秘密数学团体布尔巴基学派（Bourbaki），将严谨、抽象与逻辑奉为至高准则。该学派创始成员包括亨利・嘉当（Henri Cartan，站立者，最左侧）、安德烈・韦伊（André Weil，站立者，右数第二位）以及索莱姆・曼德尔布罗伊（Szolem Mandelbrojt，端坐者，右侧）。

布尔巴基学派的真正遗产，并非著作中的内容，而是其研究风格。该学派将抽象性置于首位，摒弃具体的例子和计算，只关注最具一般性的命题。他们呈现的每一个证明，都是一系列逻辑推导的组合，通常不会提及背后的直觉和原理。

特拉维夫大学的科学史学家利奥·科里（Leo Corry）评价道：“这是一种极具形式化的风格，刻板且严苛。”

布尔巴基学派的一本教科书

布尔巴基学派的理念迅速传播，几乎影响了全球的数学研究。巴黎-萨克雷大学的帕特里克·马索（Patrick Massot）说：“其影响力巨大，该学派最成功的研究成果，已成为数学通用知识和研究风格的一部分，让人难以想象在此之前的数学研究是何种模样。”

数学学科的体系变得愈发严密，却也愈发抽象、难以理解。数学家莫里斯·马沙尔（Maurice Mashaal）写道 https://bookstore.ams.org/bourbaki/ ：“从教学的角度来看，这绝非明智的选择。”但该学派对抽象性的强调，对研究型数学的塑造，其影响则难以评估。

一些数学家推崇布尔巴基学派的研究方法，马索认为，通过抽象化和追求优雅，“你会被迫去理解事物的核心运作逻辑，分辨何为关键、何为无关紧要的干扰信息”。在这种观点下，形式化带来了思维的清晰性。

但布尔巴基学派的研究也带来了意想不到的后果，其使用的术语和研究风格，并非适用于所有数学分支。例如，组合数学（常被描述为研究计数的科学）和图论（研究网络的科学）具有高度的具象性和直观性。因此，数十年来，这两个领域在美国和欧洲部分地区的顶尖研究机构中一直被边缘化，仅在匈牙利等布尔巴基学派影响力有限的地区得以蓬勃发展，也就不足为奇了。

孟菲斯大学的贝拉·博洛巴斯（Belá Bollobás）说：“图论曾是拓扑学的‘贫民窟’，这种状况直到最近才有所改变，真的是非常近。”

南加州大学的阿拉温德·阿索克（Aravind Asok）则担心，过度强调形式化，可能会让数学研究变得同质化。

即便是在布尔巴基框架下蓬勃发展的代数学、拓扑学、分析学等领域，一些数学家也认为该学派的影响过于深远。在他们看来，证明的撰写方式和理论的构建模式，已经变得过于单一。

阿索克说：“能明显感觉到，数学研究的文化多样性有所降低。”例如，在布尔巴基学派兴起之前，代数几何有着多种研究范式：法国的研究方法以分析学为基础，而意大利则盛行几何化的研究风格。

随着布尔巴基学派的影响力不断扩大，缺乏严谨性、存在诸多谬误的意大利代数几何学派迅速衰落。诚然，代数几何的研究因此变得更加可靠，但布尔巴基学派在切断其他潜在发展路径的同时，也带来了新的问题。阿索克表示：“我不希望数学研究被一种模式主导，数学有着值得被传承的文化历史。”

证明与前景

尽管柯西、魏尔斯特拉斯和布尔巴基学派已竭尽全力，但真正的形式化证明，始终停留在理论层面，从未成为实践主流。如今，一些数学家希望计算机能改变这一现状。

自1960年代起，研究人员便开始开发名为“证明助手”的计算机程序。数学家使用证明助手时，需用计算机能理解的语言，撰写证明的每一行内容（包括所有定义），再由程序检验逻辑的正确性。只要有一步推导无法承接上一步——哪怕是未能严谨证明1+1=2这类微小的细节，程序也不会认定该证明有效。

目前，数学家们正希望借助Lean这款证明助手，将所有数学内容形式化。他们已在Lean中构建了包含超过12万个定义的库，并验证了25万个定理。有多位数学家负责维护这一数据库，及时更新内容并审核新的研究成果（其中部分人全职从事这项工作）。该项目已获得超过1000万美元的资金支持，大部分来自亿万富翁金融家阿列克谢·格尔科（Alex Gerko）。

证明助手的工作原理

证明助手Lean通过检验数学家的推导过程、自动化证明中的部分步骤，协助其证明定理。

1. 数学家在Lean中搭建证明的基本框架，设定推导步骤的顺序

2. Lean的数学库（mathlib）中包含名为“策略”（tactic）的程序，可执行证明中的具体推导步骤

3. 核心算法依据简单的规则，检验证明的正确性

4. 验证通过的定理，会被纳入mathlib数学库中

（mathlib：用Lean语言编写的数学知识库，数学家会持续为其补充新的知识）

图源：Samuel Velasco / Quanta Magazine 译制：zzllrr小乐公众号

罗格斯大学的阿列克谢·康托罗维奇（Alex Kontorovich）称，Lean具有“革命性”，部分原因在于它能将单个证明拆解为多个部分，各部分可独立处理、验证，还能在其他证明中复用。“试想一下，倘若每次建造宇宙飞船，每位工程师都必须了解每一个组件的全部细节——从铁矿石的开采、冶炼，到组件的设计。而如今，借助这些形式化体系，数学家们首次可以像‘外购零件’一样开展研究，无需事事亲力亲为。”

但在Lean中撰写并审核定义和证明，通常需要数月时间（有些情况下只需几周，有些则超过一年）。因此，一些数学家担心，将时间和资源投入其中得不偿失。他们认为，尽管证明验证很重要，但人工检验的方式一直运转良好。阿索克表示，尽管“数学文献中存在大量谬误，但我的经验是，数学体系具有惊人的稳健性”，换言之，数学这座大厦完全崩塌的风险微乎其微。

尽管如此，Lean的使用也催生了新的数学研究成果。2019年，数学家彼得·舒尔茨（Peter Scholze）手工撰写了一个定理的证明，该定理本将成为其新数学理论的核心。但这个证明极为复杂，舒尔策也难以确定其正确性。于是在2020年末，由约翰·科梅林（Johan Commelin）和亚当·托帕兹（Adam Topaz）领衔的数学家团队，着手在Lean中对该证明进行形式化验证。数月后，他们证实了证明的正确性，让数学家们对舒尔策的新理论更有信心，且在这一过程中，他们找到了更简洁的证明方式，完善了舒尔策最初的一些想法。

伦敦帝国理工学院的凯文·巴扎德（Kevin Buzzard）是Lean的坚定支持者，他说：“形式化会迫使你用正确的方式思考数学，也会迫使你成为一名‘艺术家’。”过去一年，巴扎德一直致力于用Lean对费马大定理的证明进行形式化处理 https://imperialcollegelondon.github.io/FLT/ ——这一重要数学成果的证明过程，以冗长复杂著称。

凯文・巴扎德（Kevin Buzzard）目前正借助 Lean 工具对费马大定理的证明过程进行形式化处理，这一定理是数学领域最负盛名的成果之一。“我希望这个论证能成为一件精妙的杰作，” 他说，“我希望它能通俗易懂、令人信服。”

此外，当下为开发Lean投入时间和精力，或许是一项极具价值的投资，因为人工智能在未来的数学研究中，必将扮演更重要的角色。当数学家尝试借助人工智能撰写非形式化证明时，用Lean这类程序验证其准确性，会变得愈发重要（况且，人工智能已开始助力更高效地撰写Lean证明）。

尽管如此，Lean的广泛应用也伴随着风险：它是否会像布尔巴基学派一样，悄然改变数学家们的研究选题倾向？

不断演变的“生命体”

在Lean的体系中，数学研究的概念、方法和理念多样性，几乎没有生存空间。

一方面，Lean中每一个新证明，都只能使用已验证并存储在其库中的形式化定义和定理，这意味着这些定义和证明必须能无缝衔接；另一方面，更新或修改一个定义，会引发多米诺骨牌效应：基于旧定义撰写的证明，可能无法适配新定义。

这可能会成为一大问题。西蒙弗雷泽大学的斯蒂芬妮·迪克（Stephanie Dick）表示，数学“并非一个固定、有限、已完成形式化的体系，而是一个不断演变的生命体，其研究范畴始终在变化”。

斯蒂芬妮・迪克（Stephanie Dick）担忧，证明助手这类新技术，可能会潜移默化地影响数学家在研究中选择探索的问题方向。

图源：埃里克・苏卡 Eric Sucar / 宾夕法尼亚大学

正因如此，此前尝试将数学成果数字化的项目（例如1994年提出的QED声明 https://www.cs.ru.nl/~freek/qed/qed.html ），很快就陷入了关于“使用何种定义和框架”的争论。迪克说：“从原则上讲，所有人都认同这一想法，但实际操作起来却困难重重。人们会在编程语言的选择上产生分歧，甚至对这类项目是否具备可行性，也存在根本性的争议。”

为避免此类分歧，一群专注的Lean使用者负责确定哪些定义应纳入Lean的库，以及如何对这些定义进行编码——卡内基梅隆大学的西蒙·德迪奥（Simon DeDeo）表示，这一模式与维基百科的运营方式类似。

约翰斯·霍普金斯大学的数学家埃米莉·里尔（Emily Riehl）说：“这确实是一个社群，成员都在为社群的整体利益努力。”截至目前，这一模式运转良好，决策过程也基本保持民主。但她也表示：“其弊端在于，最终只会得出一个决策，而很多情况下，并不存在唯一正确的答案，有人会满意，就必然有人失望。”

正如布尔巴基学派的方法仅适用于特定数学领域，Lean的语言体系及其库中的定义选择，也并非对所有数学分支都同样适用：例如，它对数论和代数几何的适配性较好，对图论和范畴论则不然。

这只是Lean可能让数学研究变得同质化的一个方面。迪克指出，过往的技术——即便是数学符号的选择，也悄然改变了数学家的研究方式。Lean可能会在数学家未察觉的情况下，促使他们专注于研究那些更易形式化的概念。她说：“我已经发现了许多类似的案例，研究重心、直觉和理解方式，会从数学问题本身，转向这个系统的运行规则。”

Lean无疑带来了诸多值得期待的可能，但里尔认为，数学家们应尝试使用多种证明助手，而非单纯依赖Lean。不过，考虑到形式化研究需要投入大量精力，她也不确定这一想法的可行性。

过度修正

数个世纪以来，数学家们一直将“能否验证证明的每一步”作为追求严谨性的核心标准，但并非向来如此。对17世纪的笛卡尔而言，严谨意味着能在头脑中构建一个概念，并直观理解其成立的原因。普林斯顿高等研究院的阿克沙伊·文卡特什（Akshay Venkatesh）表示，正因如此，早期的数学证明“带有一种质朴的厚重感”。

他说：“这类证明并非形式上优雅的论证，却能让普通人轻松理解。”诚然，现代的数学证明更加优雅，却也愈发晦涩，难以让人理解其核心。（有趣的是，巴扎德在谈及对Lean影响证明撰写方式的期待时，也用到了类似的表述：“我希望这个论证成为一件美的作品，能让人轻松理解、心悦诚服。”）

这一趋势，反映出一个如今被视为理所当然的观点：证明应是数学的核心。文卡特什说：“毫无疑问，证明的概念是数学的基础组成部分，但值得质疑的是，它是否应成为定义数学的唯一特征。”

借助Lean进行形式化，将延续这种以证明为核心的趋势，但这并非数学家们设想的数学发展唯一未来。阿索克表示，研究者们被灌输了一种观念——“数学研究的唯一发展方向，是让论文都通过Lean完成形式化验证”。“而我认为，另一种可行的方向是，我们稍作停顿，减少研究成果的产出。但这与当下的学术激励机制相悖。”

我们无法预测Lean形式化会以何种方式影响数学发展，但从历史中可以明确的是，数学具有自我修正的能力，而这一轮形式化浪潮的未来，终将超出我们的想象。

参考资料

https://www.quantamagazine.org/in-math-rigor-is-vital-but-are-digitized-proofs-taking-it-too-far-20260325/

小乐数学科普近期文章

·开放 · 友好 · 多元 · 普适 · 守拙·