严谨性的革命：数学如何学会在美感与逻辑间寻找平衡

在古希腊，欧几里得证明了，如果你同意一小份初步原则（即公理），你就可以使用演绎推理来揭示各种全新的数学真理。但是，尽管这些早期的“证明”（数学家对它们的称呼）是利用逻辑定律推导出来的，它们有时也包含着隐藏的、未阐明的假设，或者依赖于误导性的直觉。在这种情况下，证明中微小的漏洞可能会被忽视；人们无法以绝对的信心说它是正确的。

在过去的几个世纪里，数学家一直试图弥补这些漏洞。到了 20 世纪初，他们确定了想要使用的公理。他们还引入了不同的逻辑系统和标准，试图进一步“形式化”（formalize）他们的论证——以确保如果你使证明中的每一次推演都清晰明确，那么无论结论多么冗长和复杂，它都必然是正确的。

这种形式化的努力赢得了信任。但它所做的远不止于此。形式化的推动帮助数学家发现了不同数学领域之间新颖的联系。它将这一领域带向了意想不到的新方向。明尼苏达州麦卡莱斯特学院的大卫·布雷苏德（David Bressoud）表示，它教会了我们：“你通常不知道自己不知道什么。要对此保持谦逊。”

但是，数学的重大进步不可避免地需要大胆的想法。这些想法通常来自实验和直觉——来自对新颖数学世界的探索和对新颖理论的测试，即使你无法证明旅程中的每一步在逻辑上都紧随上一步。这是一种不太正式的数学研究方式，起初往往包含错误。

要在描绘新数学景观所需的创造力与确保所得画面真实所需的严谨性之间取得有效的平衡并非易事。有时，形式化会破坏这种平衡。一些数学家将其视为迈向更高确定性的举动，而另一些人则将其视为卖弄学问或进步的障碍。

欧几里得的《几何原本》标志着西方数学形式化的首次重大努力。它建立了一种至今仍在使用的证明命题的演绎方法。上图为该著作 1482 年首个印刷版的页面。福格尔莎士比亚图书馆 / 知识共享 CC BY-SA 4.0

今天，数学家们正在尝试迄今为止最雄心勃勃的形式化项目。他们的目标是用一种名为 Lean 的计算机语言重写所有数学，然后由该语言自动验证他们的证明。在 Lean 中编写证明需要投入大量的时间和精力，但到目前为止，该程序已被用于验证超过 260,000 条定理。它有潜力将数学置于人们所能想象的最坚实的基础之上。

与过去形式化数学的尝试一样，Lean 引起了复杂的感受。一些数学家期待着将繁琐的验证工作交给计算机，并将 Lean 视为一种具有潜在变革性的数学研究新方式。另一些人则认为他们的时间和资源应该花在别处——或者更糟的是，认为以 Lean 为中心的方法会扭曲数学的真正价值。这场讨论正在全球各大学数学系的走廊里展开：我们如何平衡发现新数学联系所需的创造力与确保每一步逻辑都无懈可击所需的严谨性？

设定极限

寻求严谨性的一个重要里程碑，源于有史以来最重要的数学成就之一所隐藏的问题。

17 世纪末，艾萨克·牛顿和戈特弗里德·莱布尼茨独立发展了微积分（calculus），这是一种理解函数在给定点变化快慢的技术。但在非正式意义上，微积分已经存在了几个世纪。事实上，阿基米德在公元前三世纪就在做类似微积分的事情。为了计算圆的面积，他首先研究了边为直线的形状（即多边形）的面积。通过使用边数越来越多的多边形，他在估算一个极限（limit）：圆的面积。牛顿和莱布尼茨采取了类似的方法，利用极限来理解变化。

在他名为《论旋转体与球体》的论文中（此处为 1897 年的译本），阿基米德提出了数千年后在微积分发展中发挥关键作用的思想。出自 T.L. Heath 编辑的《阿基米德著作集》。剑桥大学出版社，1897 年/公有领域

微积分立即在数学和物理学中变得非常有用。但按现代标准来看，它并不正式：莱布尼茨和牛顿的论文掩盖了一些含糊之处。微积分依赖于无穷大和无穷小量（称为无穷小，infinitesimals）的概念，但牛顿和莱布尼茨用模糊的几何术语定义了这些概念；如果使用不当，他们的公式可能会导致荒谬的计算，例如除以零。

在 150 年间，这并没有引起任何问题。科学家们只是学会了区分何时可以有效使用微积分，何时不能。但在 19 世纪初，数学家开始遇到一些现象——例如无穷级数和奇怪的锯齿状曲线——这些现象挑战了他们对可能性的直觉。

这些遭遇发生时，艺术和科学领域正处于更广泛的质疑时期。哲学家、画家、作家和研究人员开始探测他们自认为所知之事的极限。“直觉是值得怀疑的，”哥伦比亚大学的历史学家阿尔玛·斯泰因加特（Alma Steingart）说。“有一种感觉，直觉会引导你走向错误的道路。”

戈特弗里德·莱布尼茨（左）和艾萨克·牛顿在 17 世纪独立发明了微积分。多年来，他们为了谁最先提出核心思想而争论不休。Christoph Bernhard Francke（左）；Godfrey Kneller

尼尔斯·阿贝尔（Niels Abel）、奥古斯丁-路易·柯西（Augustin-Louis Cauchy）和卡尔·魏尔斯特拉斯（Karl Weierstrass）等著名数学家意识到，为了理解工作中出现的离奇级数和曲线，他们需要回到最基本的定义。什么是函数？函数连续意味着什么？当你把无限多个物体加在一起时，到底发生了什么？

他们提出了回答这些问题的正式定义。（例如，魏尔斯特拉斯引入了极限的精确定义，学生至今仍在使用。）他们的新定义使数学家能够以比以往更深入、更严谨的方式研究函数——最终孕育了分析学（analysis）领域。

今天，分析学是数学中最重要的领域之一。它让数学家能够理解从流体流动和电流到遥远星球化学成分的一切事物。它与几乎所有其他类型的数学都有深刻的联系，包括古老的数论和几何领域。

微积分的形式化还导致了集合论（set theory）的诞生，它确立了现代数学的基础规则。集合论现在本身就是一个活跃的研究领域。

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

尽管如此，一些研究人员也对这一新形式化浪潮感到忧虑。“在热情被严谨主义者的‘湿毯子’（泼冷水）人为冷却后，想要提振起任何热情都是不容易的，”物理学家奥利弗·赫维赛德（Oliver Heaviside）在 1899 年写道。

正如历史学家耶斯佩尔·吕岑（Jesper Lützen）在回顾这一时期时所观察到的：“分析学既获得了严谨性，也获得了普遍性，但它失去了优雅和简洁，并与直觉疏远。许多数学家对此倾向感到遗憾，但却难以逃脱。”

至关重要的是，严谨主义者及其反对者找到了折衷方案：数学家继续使用柯西和魏尔斯特拉斯细致的定义，但他们也开发了一些框架，允许赫维赛德这样的科学家更自由地利用无穷大和无穷小进行计算。

换句话说，形式化并非他们唯一的目标。事实上，故事的一个重要部分是形式化背后的意图。它的焦点相对狭窄：魏尔斯特拉斯及其同事一直在处理关于函数行为的非常具体的问题，他们转向形式化是为了解决这些问题。从那时起，分析学、集合论和其他形式化系统的发展是自然而然发生的。

“科学的大厦并非像住宅那样拔地而起，即先牢牢打好地基，然后才开始建造和扩大房间，”伟大的数学家大卫·希尔伯特（David Hilbert）在 1905 年写道。相反，科学家应该首先发现“可以漫游的舒适空间，只有在随后某些地方出现迹象表明松动的地基无法支撑房间的扩建时，（他们才应该）支撑并加固它们。”

“这并非弱点，”他继续说道，“而恰恰是正确而健康的演进之路。”

毕竟，当一个形式化努力的目标超出了巩固松动地基的范畴时，它可能会产生非常不同的后果。

肃穆的学院

清晰度和严谨性是有可能走向极端的。

考虑数学界最著名（或者说臭名昭著，取决于你问谁）的思想流派之一，该哲学是由一个名为布尔巴基（Bourbaki）的秘密数学家协会提出的。

20 世纪 30 年代中期，法国数学界已低迷数十年。该国在一战期间失去了一代有前途的学生和研究人员；其大学教授数学的方式极不协调且零碎，使用的教材陈旧不堪。于是，几位年轻的数学家聚集在一起组成了布尔巴基。他们开始时目标谦逊：用一套更具凝聚力的新教材将法国课程带入现代。然而不久，他们的雄心壮志便增长了许多。今天，布尔巴基（其成员身份仍然保密）已经出版了 40 多卷著作，涵盖了所有可以想象的数学领域。

创建于 20 世纪 30 年代的秘密数学协会“布尔巴基”将严谨、抽象和逻辑置于一切之上。其创始成员包括亨利·嘉当（站立者，最左）、安德烈·韦伊（站立者，右二）和佐莱姆·曼德勃罗（坐者，右）。

然而，这些书真正的遗产不在于它们的内容，而在于它们的风格。布尔巴基将抽象化置于一切之上，回避具体的例子和计算，转而只采用最普遍的陈述。他们将每个证明呈现为一系列逻辑推演，通常不引用任何潜在的直觉或基本原理。

“这是一种非常形式化的风格，”特拉维夫大学的历史学家利奥·科里（Leo Corry）说。“非常肃穆。”

布尔巴基的哲学迅速传播，几乎影响了各地的数学。“它产生了巨大的影响，”巴黎-萨克雷大学的帕特里克·马索（Patrick Massot）说。“其中最成功的部分已成为公共数学知识和风格的一部分，以至于很难想象以前是什么样子。”

这一学科变得更加严丝合缝，尽管也日益抽象和困难。“从教学的角度来看，这并不是一个英明的决定，”《科学》杂志（Pour la Science）的长期编辑、关于布尔巴基书籍的作者莫里斯·马沙尔（Maurice Mashaal）写道。但该小组对抽象的强调塑造研究数学的方式，则难以评估。

一些数学家推崇布尔巴基的方法。马索认为，通过抽象和优雅，“你被迫去理解真正让事物运作的原因，以及哪些只是噪音。”在这一观点中，形式化带来了清晰。

但布尔巴基的项目也产生了意想不到的后果。他们的词汇和风格并不适合每一种类型的数学。例如，组合数学（通常被描述为计数的科学）和图论（网络的科学）往往是高度具体和直观的。那么，也就不奇怪在几十年的时间里，它们在美国和欧洲部分地区最负盛名的机构中都被边缘化了；它们只能在布尔巴基影响力有限的地方（如匈牙利）蓬勃发展。

“图论（曾）是拓扑学的贫民窟，”剑桥大学的贝拉·博洛巴什（Béla Bollobás）说。“那种氛围直到最近才改变。非常最近。”

即使在确实在布尔巴基框架下蓬勃发展的领域——代数、拓扑、分析——一些数学家也担心布尔巴基过于成功了。根据他们的说法，撰写证明和构建理论的方式已经变得过度同质化。

“有一种感觉，它降低了数学的文化多样性，”南加州大学的阿拉温德·阿索克（Aravind Asok）说。例如，在布尔巴基之前，代数几何有许多版本。在法国，方法植根于分析学，而在意大利，几何风格占据主导地位。

随着布尔巴基影响力的传播，缺乏严谨性且包含许多错误的意大利学派迅速消退。当然，代数几何变得更加可靠。但通过切断其他可能的进步路径，布尔巴基引入了一个新问题。“我不想要任何一种模式主导的数学，”阿索克说。“数学有一种值得保留的文化历史。”

证明与承诺

尽管布尔巴基、柯西和魏尔斯特拉斯做出了最大的努力，但真正形式化的证明一直是理论上的对象，而非实践中的。一些数学家现在希望计算机能改变这一点。

自 20 世纪 60 年代以来，研究人员一直在开发名为证明辅助工具（proof assistants）的计算机程序。使用证明辅助工具，数学家会用计算机能理解的语言编写证明的每一行（包括每个定义），然后证明辅助工具将检查逻辑。即使只有一步不符合前一步——如果你没有严谨地展示每一个微小的细节，比如 1 + 1 等于 2 这个事实——那么程序就不会认为证明是正确的。

目前，数学家希望使用名为 Lean 的证明辅助工具将所有数学形式化。到目前为止，他们已经创建了一个包含 120,000 多个定义的库，并验证了 25 万条定理。几位数学家维护着这个数据库，保持更新并审核新的贡献。（其中少数人全职从事这项工作。）他们已经获得了超过 1000 万美元的资金，主要来自亿万富翁金融家亚历克斯·格科（Alex Gerko）。

Samuel Velasco / Quanta Magazine

罗格斯大学的亚历克斯·康托罗维奇（Alex Kontorovich）表示，Lean 是“革命性的”，部分原因是它将单个证明分解成许多部分，每个部分都可以单独处理、独立验证并在其他证明中重复使用。“想象一下，如果每次你想建造一艘宇宙飞船，每个工程师都必须了解每一个组件——从开采铁矿石到熔炼、设计。现在有了这些形式化系统，你第一次可以在做数学时，直接从货架上买下别人的零件。”

但在 Lean 中编写和审核定义和证明通常需要数月时间。（在某些情况下，形式化一个证明仅需几周；而在其他情况下，则需要一年以上。）因此，一些数学家担心他们的时间和资源花在其他追求上会更好。他们认为，虽然验证证明很重要，但人工检查已经做得足够好了。阿索克说，尽管“文献中有很多很多错误，但我的经验是，数学具有非凡的鲁棒性。”换句话说，数学的大厦并无崩塌的危险。

尽管如此，使用 Lean 也催生了新的数学。2019 年，数学家彼得·肖尔茨（Peter Scholze）亲手写下了一个定理的证明，该定理注定在他正在开发的一种新数学理论中发挥关键作用。但证明极其复杂，他难以确定它是否正确。因此在 2020 年底，由 Johan Commelin 和 Adam Topaz 领导的一组数学家着手在 Lean 中将该证明形式化。几个月后，他们确认它是正确的，让数学家对肖尔茨的新理论有了更大的信心。在此过程中，他们发现了一个更简洁的证明，并精炼了肖尔茨的一些原始想法。

“它迫使你以正确的方式思考数学，”伦敦帝国理工学院的数学家、Lean 最坚定的倡导者之一凯文·巴扎德（Kevin Buzzard）说。“它迫使你成为一名艺术家。”（巴扎德在过去的一年里一直致力于使用 Lean 将费马大定理的证明形式化，这是一个重要结果，其证明以冗长复杂著称。）

凯文·巴扎德目前正在使用 Lean 形式化费马大定理的证明，这是数学中最著名的结果之一。“我希望这个论证能成为一件美妙的事物，”他说，“我希望它能顺滑地滑入喉咙（意为极易理解）。” 由凯文·巴扎德提供

此外，现在花时间开发 Lean 可能是对未来的一项良好投资，因为人工智能必然会在数学中发挥更大的作用。当数学家尝试使用 AI 编写非正式证明时，使用 Lean 这样的程序来验证其准确性将变得更加重要。（此外，AI 已经在帮助更高效地编写 Lean 证明了。）

尽管如此，Lean 的广泛采用也伴随着风险。Lean 是否会像布尔巴基一样，微妙地改变数学家觉得有趣的问题类型？

一个“移动、变化的怪兽”

在 Lean 内部，几乎没有给概念、方法论或意识形态多样性留出空间。

首先，Lean 中的每一个新证明都只能使用已经验证并存储在其库中的正式定义和定理。这意味着这些定义和证明需要无缝地契合在一起。这也意味着更新或更改一个定义会产生多米诺骨牌效应：使用旧定义编写的证明可能无法与新定义协同工作。

这可能是一个问题。西蒙菲莎大学的斯蒂芬妮·迪克（Stephanie Dick）表示，数学“不是一个固定、有限且形式化的事业。它是一个移动、变化的怪兽，其术语一直在改变。”

斯蒂芬妮·迪克警惕着诸如证明辅助工具之类的新技术，可能会如何微妙地影响数学家在研究中提出的问题。Eric Sucar/宾夕法尼亚大学

正因为如此，之前将数学结果数字化的尝试（例如 1994 年一个名为 QED 宣言的项目）很快演变成了关于使用哪些定义和框架的争论。“原则上每个人都喜欢这个想法，但在实践中，它是场噩梦，”迪克说。“他们在应该用哪种编程语言编写上存在分歧……在这一类项目是否可能实现上，存在根本性的分歧。”

为了避免这些分歧，一个专门的 Lean 用户小组负责决定哪些定义应该进入 Lean 的库，以及这些定义应该如何编码——卡内基梅隆大学的西蒙·德迪奥（Simon DeDeo）说，这很像维基百科的做法。

“这确实是一个试图为社区做最好事情的社区，”约翰·霍普金斯大学的数学家艾米莉·里尔（Emily Riehl）说。到目前为止，它是有效的，而且过程在很大程度上是民主的。但是，她说，“坏处在于，最终会做出一个决定，而在许多情况下，并没有一个唯一的正确决定。有些人会高兴，而另一些人会不高兴。”

正如布尔巴基的方法对某些学科是最佳的，而对其他学科则不然，Lean 语言以及进入其库的定义选择对某些数学领域比其他领域更合适。例如，它们非常适合数论和代数几何。图论和范畴论则没那么契合。

这只是 Lean 可能使数学更加同质化的一种方式。迪克指出，过去的技术——甚至是选择使用哪种符号系统——都微妙地改变了数学家处理工作的方式。Lean 可能会鼓励他们专注于开发更容易形式化的概念，即使他们自己没有意识到这一点。“我现在已经发现了许多此类情况，”她说，“它实际上将焦点、直觉和理解从数学问题领域转移到了系统的行为上。”

在 Lean 方面，确实有很多值得兴奋的地方。但里尔认为，数学家应该尝试使用多种证明辅助工具，而不是仅仅依赖于 Lean。然而，考虑到形式化需要投入多少精力，她不确定这在实践中会有多可行。

关于过度矫正

几个世纪以来，数学家一直通过关注是否能验证证明的每一行来寻求更高的严谨性。但这并不总是如此。对于 1600 年代的笛卡尔来说，严谨意味着能够在大脑中保持一个想法，并直观地理解它为什么是真的。因此，根据普林斯顿高等研究院的阿克沙伊·文卡特什（Akshay Venkatesh）的说法，旧的证明过去往往“有一种颗粒感”。

“这并不能形成形式上优雅的论证，”他说。但它是“人类可以轻松理解的东西”。现代证明确实更优雅，但它们也更滑溜，思维更难抓牢。（有趣的是，巴扎德在讨论他希望 Lean 如何影响证明撰写时也使用了类似的语言。“我希望这个论证能成为一件美妙的事物，”他说，“我希望它能顺滑地滑入喉咙。”）

这一趋势反映了一个现在被视为理所当然的概念：证明应该处于数学的核心。“毫无疑问，证明的概念是数学的一个基本部分，”文卡特什说。但是，“我认为值得怀疑的地方在于，它是否应该成为数学的定义性特征。”

在 Lean 中进行形式化将继续这种优先考虑证明的趋势。但这不是数学家们想象的唯一未来。阿索克说，研究人员被鼓励去认为“唯一的出路就是让论文经过 Lean 形式化。我认为另一种方式是我们退后一步，停止写那么多东西。但这与现有的激励机制是背道而驰的。”

要预测 Lean 的形式化可能影响数学的所有方式是不可能的。从历史中可以清楚地看到，数学具有自我修正的倾向——而下一次形式化浪潮的未来，将是我们尚未想象到的未来。

编者注：Alex Kontorovich 是《量子杂志》顾问委员会的成员。

更正： 2026 年 3 月 27 日 本故事的早期版本将莫里斯·马沙尔称为数学家。他实际上是一名记者。此外，贝拉·博洛巴什的隶属机构已更新，以反映他主要隶属于剑桥大学。

---

重要术语翻译表

英文术语	中文翻译	定义/背景
Axiom	公理	证明的起始假设，不证自明。
Formalization	形式化	将数学论证转化为严格的逻辑步骤的过程。
Deductive reasoning	演绎推理	从一般原则推导出特定结论的过程。
Calculus	微积分	研究变化的数学分支，由牛顿和莱布尼茨奠基。
Analysis	分析学	研究极限、连续性和函数的严谨数学分支。
Limit	极限	数列或函数无限接近某个值的概念。
Infinitesimal	无穷小	极小但非零的量，早期微积分的争议概念。
Set theory	集合论	研究集合及其性质的数学分支，现代数学的基石。
Bourbaki	布尔巴基	20世纪著名的秘密数学家小组，强调极致的抽象。
Proof assistant	证明辅助工具	能够自动检查数学证明逻辑的计算机软件。
Lean	Lean 语言	一种现代的数学形式化编程语言。
Algebraic geometry	代数几何	用多项式方程研究几何对象的领域。
Combinatorics	组合数学	研究离散对象的计数、排列和组合。
Graph theory	图论	研究顶点和边组成的网络的科学。
Fermat’s Last Theorem	费马大定理	著名的数论猜想，由怀尔斯于1994年最终证明。
Rigor	严谨性	数学论证的严密程度和逻辑完整性。