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

内容总结：

数学严谨性之争：当证明走向数字化，我们是否在扼杀创造力？

自欧几里得以公理化体系奠基数学证明以来，数学家们始终在追求逻辑的绝对严谨。从牛顿、莱布尼茨微积分中“无穷小”概念的模糊，到19世纪柯西、魏尔斯特拉斯用严格极限定义重塑分析学，数学史一次次证明：严谨化进程虽常始于修补漏洞，却往往能催生全新领域，如分析学与集合论的诞生。

然而，历史的教训同样深刻。20世纪中叶，法国数学团体“布尔巴基”以极度抽象、剔除直觉的写作风格席卷学界，虽提升了论证的严密性，却也让组合数学等依赖直观的领域长期边缘化。这揭示了一个永恒难题：在探索的创造力与证明的严谨性之间，应如何平衡？

如今，一场更彻底的变革正在发生。借助名为“Lean”的计算机证明辅助系统，全球数学家正尝试将全部数学形式化编码。该系统已核验超过26万条定理，并能将证明拆分为可复用模块，被誉为“革命性工具”。支持者认为，Lean不仅能杜绝疏漏，还能通过形式化过程揭示新数学联系——例如，彼得·舒尔兹一项复杂证明经Lean验证后，其理论更趋完善。

但质疑声同样强烈。编写Lean证明耗时巨大，可能分散研究者探索新问题的精力。更深的忧虑在于：统一的形式化语言是否会像布尔巴基那样，无形中压制数学方法的多样性？Lean目前对代数几何等领域适配良好，却难以兼容图论等依赖直观的学科。有学者警告，过度依赖单一系统可能使数学思考“从问题本身转向系统行为”。

这场争论触及数学的本质：证明是否应成为数学的唯一核心？17世纪的笛卡尔曾将“直观理解”视为严谨，而现代证明虽逻辑完美却常丧失这种可触感。Lean的推进，或许将加速数学向“可验证性”倾斜，但历史表明，数学始终在自我修正中前进。

正如数学家希尔伯特所言：“科学大厦的建造并非从夯实地基开始，而是先寻找可漫步的舒适空间。”在数字化严谨与人类直觉的张力间，数学的未来仍是一场未完成的探索。

中文翻译：

在数学领域，严谨性至关重要。但数字化的证明是否走得太远？

克里斯蒂娜·阿米蒂奇 / 量子杂志

在古希腊，欧几里得证明，只要认同一小列初步原理或公理，就可以运用演绎推理揭示各种新的数学真理。但尽管这些早期证明——数学家们这样称呼它们——是依据逻辑法则推导出来的，它们有时也包含隐藏的、未言明的假设，或依赖于误导性的直觉。在这些情况下，证明中的微小漏洞可能被忽视；人们无法绝对自信地说它是正确的。

过去几个世纪以来，数学家们一直致力于填补这些漏洞。到20世纪初，他们确定了想要使用的公理。他们还引入了不同的逻辑系统和标准，以进一步“形式化”他们的论证——确保如果你将证明中的每一步演绎都明确化，那么无论证明变得多么冗长和复杂，其结论都必然为真。

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

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

在描绘新数学图景所需的创造力和确保最终图景为真所需的严谨性之间，要取得富有成效的平衡并非易事。有时，形式化可能会打破这种平衡。一些数学家视为迈向更高确定性的举措，另一些人可能视为迂腐或进步的障碍。

福尔杰莎士比亚图书馆 / Cretive Commons CC BY-SA 4.0

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

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

设定界限

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

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

来自T.L. Heath编辑的《阿基米德著作集》。剑桥大学出版社，1897年/公共领域

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

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

这些遭遇发生之时，正值艺术和科学领域更广泛的质疑时期。哲学家、画家、作家和研究人员开始探究他们自认已知事物的界限。“直觉是可疑的，”哥伦比亚大学历史学家阿尔玛·斯坦加特说。“有一种感觉，直觉可能会把你引向错误的方向。”

克里斯托夫·伯恩哈德·弗兰克（左）；戈弗雷·内勒

尼尔斯·阿贝尔、奥古斯丁-路易·柯西和卡尔·魏尔斯特拉斯等著名数学家意识到，要理解他们工作中不断出现的奇异级数和曲线，他们需要回到最基本的定义。什么是函数？函数连续意味着什么？当你把无限多个对象相加时，到底发生了什么？

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

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

微积分的形式化也导致了集合论的诞生，它确立了现代数学所依据的规则。集合论本身现在也是一个活跃的研究领域。

史密森尼图书馆（左）；公共领域

尽管如此，一些研究人员也以忧虑的心情面对这股新的形式化浪潮。“在被严谨主义者的湿毯子人为冷却之后，很难再激起任何热情，”物理学家奥利弗·亥维赛在1899年写道。

正如历史学家杰斯珀·吕岑回顾这一时期时所指出的：“分析学既获得了严谨性又获得了普遍性，但它失去了优雅和简洁，并与直觉疏远。许多数学家对这种趋势感到遗憾，但却难以逃脱。”

关键的是，严谨主义者及其批评者找到了一个折衷方案：数学家们继续使用柯西和魏尔斯特拉斯的谨慎定义，但他们也发展了允许像亥维赛这样的科学家更自由地计算无穷和无穷小量的框架。

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

“科学大厦的建造不像住宅，先牢固地打好地基，然后才着手建造和扩大房间，”伟大的数学家大卫·希尔伯特在1905年写道。相反，科学家应该首先找到“舒适的空间四处漫游，然后，只有当各处迹象表明松散的地基无法支撑房间的扩张时，才去支撑和加固它们。”

“这不是弱点，”他继续说，“而是正确且健康的发展道路。”

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

刻板的学院派

清晰和严谨也可能走得太远。

想想数学中最著名（或最臭名昭著，取决于你问谁）的思想流派之一，这是一个名为布尔巴基的数学家秘密社团提出的哲学。

在20世纪30年代中期，法国的数学已经萎靡了数十年。该国在第一次世界大战中失去了一代有前途的学生和研究人员；其大学以不协调、零散的方式教授数学，使用的材料严重过时。因此，几位年轻数学家联合起来组成了布尔巴基。他们最初的目标很朴素：用一本新的、更具凝聚力的教科书将法国课程带入现代。然而很快，他们的野心变得大得多。今天，布尔巴基（其成员仍然保密）已经出版了40多卷，涵盖了所有可以想象的数学领域。

尼古拉·布尔巴基

然而，这些书籍的真正遗产不是其内容，而是其风格。布尔巴基将抽象置于一切之上，避开具体的例子和计算，只青睐最一般的陈述。他们将每个证明呈现为一系列逻辑演绎，通常不提及任何潜在的直觉或原理。

“这是一种非常形式化的风格，”特拉维夫大学历史学家利奥·科里说。“非常刻板。”

布尔巴基的哲学迅速传播，几乎影响了所有地方的数学。“它产生了巨大的影响，”巴黎-萨克雷大学的帕特里克·马索说。“最成功的部分已经如此深入地融入了普通的数学知识和风格，以至于很难想象之前是什么样子。”

这门学科变得严密得多，尽管也越来越抽象和困难。“从教学角度来看，这不是一个明智的决定，”数学家莫里斯·马沙尔写道。但该团体对抽象的强调以难以评估的方式塑造了研究数学。

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

但布尔巴基的项目也带来了意想不到的后果。他们的词汇和风格并不天然适合每一种数学。例如，组合数学（通常被描述为计数的科学）和图论（网络科学）往往高度具体和视觉化。因此，也许不足为奇的是，几十年来，它们在美国和欧洲部分地区的多数知名机构中被边缘化；它们只能在布尔巴基影响有限的地方蓬勃发展，比如匈牙利。

“图论[曾经]是拓扑学的贫民窟，”孟菲斯大学的贝拉·博洛巴什说。“那种氛围直到最近才改变。非常近。”

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

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

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

证明与承诺

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

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

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

塞缪尔·维拉斯科 / 量子杂志

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

但用Lean编写和审核定义及证明通常需要数月时间。（在某些情况下，形式化一个证明只需几周；在其他情况下，则需要一年多。）因此，一些数学家担心他们的时间和资源最好花在其他追求上。他们认为，虽然验证证明很重要，但手工检查已经足够有效。尽管“文献中有很多很多错误，”阿索克说，“但我的经验是，数学具有显著的稳健性。”换句话说，整个数学大厦轰然倒塌的危险很小。

尽管如此，使用Lean也催生了新的数学。2019年，数学家彼得·舒尔茨手写了一个定理的证明，该定理在他正在发展的新数学理论中扮演关键角色。但这个证明极其复杂，他难以确定其是否正确。因此，在2020年底，由约翰·科梅林和亚当·托帕兹领导的一个数学家团队着手在Lean中形式化这个证明。几个月后，他们确认证明是正确的，这使数学家们对舒尔茨的新理论有了更大的信心。在这个过程中，他们找到了一个更简洁的证明，并完善了舒尔茨的一些原始想法。

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

由凯文·巴扎德提供

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

然而，Lean的广泛采用也伴随着风险。Lean是否会像布尔巴基一样，微妙地改变数学家们感兴趣的问题类型？

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

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

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

这可能是个问题。数学“不是一个固定的、有限的和形式化的事业，”西蒙弗雷泽大学的斯蒂芬妮·迪克说。“它是一个移动、变化的野兽，其术语一直在变化。”

埃里克·苏卡 / 宾夕法尼亚大学

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

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

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

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

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

关于Lean，当然有很多令人兴奋的地方。但里尔认为，数学家们应该尝试使用不止一种证明助手，而不是仅仅依赖Lean。然而，考虑到形式化需要付出多少努力，她不确定这有多实际。

关于矫枉过正

几个世纪以来，数学家们一直通过关注是否能验证证明的每一行来寻求更高的严谨性。但情况并非总是如此。对17世纪的笛卡尔来说，严谨意味着能够将一个想法记在脑中，并直观地理解它为什么是真的。因此，根据高等研究院的阿卡什·文卡特什的说法，古老的证明过去常常“有一种粗糙感”。

“它不会形成一个形式上优雅的论证，”他说。但它是“人类可以轻易理解的东西。”现代证明当然更优雅。但它们也更滑溜，更难让思维把握住。（有趣的是，巴扎德在讨论他对Lean如何影响证明写作的期望时使用了类似的语言。“我希望这个论证是一件美丽的东西，”他说。“我希望它能顺畅地滑下喉咙。”）

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

Lean中的形式化将继续这种优先考虑证明的趋势。但这并不是数学家们设想的唯一未来。研究人员被鼓励认为“前进的唯一途径是让论文被Lean形式化，”阿索克说。“我会提出另一种方式，那就是我们退一步，少写一些。但这与现有的激励机制背道而驰。”

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

编者注：亚历克斯·孔托罗维奇是《量子杂志》顾问委员会的成员。

英文来源：

In Math, Rigor Is Vital. But Are Digitized Proofs Taking It Too Far?
Kristina Armitage/Quanta Magazine
In ancient Greece, Euclid showed that if you agree on a small list of preliminary principles, or axioms, you can use deductive reasoning to reveal all sorts of new mathematical truths. But although these early proofs, as mathematicians call them, were derived using the laws of logic, they sometimes also contained hidden, unstated assumptions or relied on misleading intuitions. In these cases, small gaps in a proof might go unnoticed; one couldn’t say with absolute confidence that it was correct.
Over the past few centuries, mathematicians have sought to close those gaps. By the early 1900s, they settled on the axioms they wanted to use. They also introduced different logical systems and standards in an effort to further “formalize” their arguments — to guarantee that, if you made every deduction in a proof explicit, its conclusion would have to be true no matter how long and convoluted it got.
This formalization effort engendered trust. But it did far more than that. The push to formalize has helped mathematicians uncover novel connections between different areas of math. It has taken the field in unexpected new directions. It has taught us, said David Bressoud of Macalester College in Minnesota, that “you often don’t know what you don’t know. And to be humble about that.”
But big advances in mathematics inevitably require bold ideas. These often come from experimentation and intuition — from exploring novel mathematical worlds and testing out novel theories, even if you can’t prove that every step in the journey logically follows from the last. It’s a less formal way of doing math that at first tends to contain mistakes.
It’s not easy to strike a fruitful balance between the creativity needed to paint new mathematical landscapes and the rigor necessary to ensure that the resulting pictures are true. Sometimes, formalization can upset that balance. What some mathematicians see as a move toward greater certainty, others might see as pedantry or a barrier to progress.
Folger Shakespeare Library / Cretive Commons CC BY-SA 4.0
Today, mathematicians are attempting their most ambitious formalization project yet. They’re aiming to rewrite all of mathematics in a computer language known as Lean, which can then automatically verify their proofs. Writing a proof in Lean requires an enormous amount of time and effort, but so far, the program has been used to verify more than 260,000 theorems. It has the potential to put mathematics on the most solid foundation one can imagine.
As with past attempts to formalize math, Lean has generated mixed feelings. Some mathematicians look forward to offloading tedious verification work onto computers and see Lean as a potentially transformative new way of doing mathematics. Others think that their time and resources are better spent elsewhere — or, worse, that a Lean-centric approach will distort the true value of mathematics. It’s a discussion that’s starting to play out in the hallways of math departments around the world: How do we balance the creativity needed to discover new mathematical connections with the rigor needed to ensure that every logical step is undeniable?
Setting Limits
A major milestone in the quest for rigor came about because of hidden problems with one of the most important mathematical achievements of all time.
In the late 17th century, Isaac Newton and Gottfried Leibniz independently developed calculus, a technique for understanding how quickly a function changes at a given point. But in an informal sense, calculus had already been around for centuries. In fact, Archimedes was doing something like calculus in the third century BCE. To calculate the area of a circle, he first studied the areas of shapes with straight sides called polygons. By using polygons with more and more sides, he was estimating a limit: the area of the circle. Newton and Leibniz took a similar approach, using limits to understand change.
From T.L. Heath’s edition of The Woks of Archimedes. Cambridge University Press, 1897/Public Domain
Calculus immediately became useful throughout math and physics. But it was not formal by modern standards: Leibniz’s and Newton’s papers glossed over some ambiguities. Calculus relies on the notions of infinity and infinitely small quantities (called infinitesimals), but Newton and Leibniz defined these concepts in vague geometric terms; used incorrectly, their formulas could lead to nonsensical calculations, like division by zero.
For 150 years, that didn’t cause any problems. Scientists simply learned to tell when calculus could be used effectively and when it couldn’t. But in the early 19th century, mathematicians started to encounter phenomena — infinite sums and strange, jagged curves, for instance — that defied their intuition for what was possible.
These encounters came at a time of broader questioning across the arts and sciences. Philosophers, painters, writers, and researchers were beginning to probe the limits of what they thought they knew. “Intuition is suspect,” said Alma Steingart, a historian at Columbia University. “There is this feeling that intuition can lead you the wrong way.”
Christoph Bernhard Francke (left); Godfrey Kneller
Renowned mathematicians such as Niels Abel, Augustin-Louis Cauchy, and Karl Weierstrass realized that to make sense of the bizarre sums and curves that were cropping up in their work, they needed to return to their most fundamental definitions. What is a function? What does it mean for a function to be continuous? What really happens when you add up infinitely many objects?
They came up with formal definitions that answered these questions. (Weierstrass, for instance, introduced the precise definition of a limit that students still use today.) Their new definitions enabled mathematicians to study functions in a much deeper and more rigorous way than they ever had before — ultimately spawning the field of analysis.
Today, analysis is one of the most important areas in math. It allows mathematicians to understand everything from fluid flow and electrical currents to the chemical makeup of far-off stars. And it is deeply connected to almost every other type of math, including the far older fields of number theory and geometry.
The formalization of calculus also led to the birth of set theory, which established the rules that underlie modern mathematics. Set theory is now an active area of study in its own right.
The Smithsonian Libraries (left); Public Domain
Still, some researchers also faced this new wave of formalization with trepidation. “It is not easy to get up any enthusiasm after it has been artificially cooled by the wet blankets of the rigorists,” the physicist Oliver Heaviside wrote in 1899.
As the historian Jesper Lützen has observed, looking back at this time period: “Analysis gained both rigor and generality, but it lost in elegance and simplicity and was estranged from intuition. Many mathematicians regretted this tendency, but it was hard to escape.”
Crucially, rigorists and their detractors found a compromise: Mathematicians continued to use the careful definitions of Cauchy and Weierstrass, but they also developed frameworks that allowed scientists like Heaviside to compute with infinity and infinitesimals more freely.
In other words, formalization wasn’t their only aim. In fact, an important part of this story is the intent behind the formalization. Its focus was relatively narrow: Weierstrass and his colleagues had been dealing with very particular questions about the behavior of functions, and they turned to formalization in order to deal with those problems. From there, the development of analysis, set theory, and other formal systems happened organically.
“The edifice of science is not raised like a dwelling, in which the foundations are first firmly laid and only then one proceeds to construct and to enlarge the rooms,” the great mathematician David Hilbert wrote in 1905. Rather, scientists should first find “comfortable spaces to wander around and only subsequently, when signs appear here and there that the loose foundations are not able to sustain the expansion of the rooms, [should they] support and fortify them.”
“This is not a weakness,” he continued, “but rather the right and healthy path of development.”
After all, a formalization effort can have very different consequences when it aims to go beyond cementing loose foundations.
The Austere Academy
It’s possible to take clarity and rigor too far.
Consider one of math’s most famous (or infamous, depending on whom you ask) schools of thought, a philosophy put forth by a secret society of mathematicians called Bourbaki.
In the mid-1930s, mathematics in France had been suffering for decades. The country had lost a generation of promising students and researchers during World War I; its universities were teaching math in uncoordinated, fragmented ways, using materials that were woefully out of date. And so several young mathematicians banded together to form Bourbaki. They began with a modest goal: to bring the French curriculum into the modern era with a new, more cohesive textbook. Soon, though, their ambitions grew much larger. Today, Bourbaki (whose members remain a secret) has produced over 40 volumes, covering every conceivable area of mathematics.
Nicolas Bourbaki
The real legacy of these books, however, is not their content but their style. Bourbaki prioritized abstraction over all else, eschewing concrete examples and calculations in favor of only the most general statements. They presented each proof as a series of logical deductions, usually without reference to any underlying intuition or rationale.
“It’s a style that is very formal,” said Leo Corry, a historian at Tel Aviv University. “Very austere.”
Bourbaki’s philosophy quickly spread, influencing mathematics almost everywhere. “It had an enormous influence,” said Patrick Massot of Paris-Saclay University. “The most successful parts have become so much part of the common mathematical knowledge and style that it’s hard to think of what it was before.”
The subject became far more airtight, if increasingly abstract and difficult. “This was not a brilliant decision from a pedagogical point of view,” wrote the mathematician Maurice Mashaal. But the group’s emphasis on abstraction molded research mathematics in ways that are harder to assess.
Some mathematicians revere Bourbaki’s approach. Massot argues that through abstraction and elegance, “you are forced to understand what really makes things work, and what is just noise.” Formalization, in this view, has brought clarity.
But Bourbaki’s project had unforeseen consequences as well. Their vocabulary and style weren’t a natural fit for every type of mathematics. For example, the fields of combinatorics (often described as the science of counting) and graph theory (the science of networks) tend to be highly concrete and visual. Perhaps, then, it’s no surprise that for decades, they were sidelined at most prestigious institutions in the United States and parts of Europe; they were only able to thrive in places where Bourbaki’s influence was limited, like Hungary.
“Graph theory [was] the slum of topology,” said Belá Bollobás of the University of Memphis. “That atmosphere changed only recently. Very recently.”
Even in fields that did flourish under the Bourbaki framework — algebra, topology, analysis — some mathematicians worry that Bourbaki was too successful. According to them, the ways in which proofs are written and theories constructed have become overly homogeneous.
“There is a sense that it decreased the cultural diversity of mathematics,” said Aravind Asok of the University of Southern California. Before Bourbaki, for instance, there were many versions of algebraic geometry. In France, for example, methods were grounded in analysis, while in Italy, a geometric style reigned.
The Italian school, which lacked rigor and involved many errors, quickly faded as Bourbaki’s influence spread. Certainly, algebraic geometry became more reliable. But by cutting off other paths of possible progress, Bourbaki introduced a new problem. “I don’t want any mathematics where one mode dominates,” Asok said. “There is a cultural history to mathematics that deserves to be preserved.”
Proofs and Promises
Despite the best efforts of Bourbaki, Cauchy, and Weierstrass, truly formal proofs have always been objects of theory, not practice. Some mathematicians now hope that computers can change that.
Since the 1960s, researchers have been developing computer programs called proof assistants. Using a proof assistant, a mathematician will write every line of a proof (including every definition) in a language that the computer can understand, and then the proof assistant will check the logic. If even a single step doesn’t follow from a preceding one — if you haven’t rigorously shown every tiny detail, like the fact that 1 + 1 equals 2 — then the program will not consider the proof correct.
Currently, mathematicians are hoping to formalize all of mathematics using a proof assistant called Lean. They’ve created a library of more than 120,000 definitions so far and have verified a quarter of a million theorems. Several mathematicians maintain this database, keeping it up to date and vetting new contributions. (A handful of them do this work full time.) They’ve received over $10 million in funding, mostly from the billionaire financier Alex Gerko.
Samuel Velasco/Quanta Magazine
Lean is “revolutionary,” said Alex Kontorovich of Rutgers University, in part because it breaks up a single proof into many pieces that can each be handled separately, verified independently, and reused in other proofs. “Imagine if every time you wanted to build a spaceship, every single engineer has to understand every single component — from mining the iron ore, to smelting it, designing it. Now with these formal systems, for the first time, you can do mathematics and just buy somebody’s part off the shelf.”
But it usually takes months to write and vet definitions and proofs in Lean. (In some cases, formalizing a proof takes only a few weeks; in others, more than a year.) Some mathematicians therefore worry that their time and resources would be better spent on other pursuits. They argue that while verifying proofs is important, checking them by hand has worked well enough. Even though “there are many, many errors in the literature,” Asok said, “my experience is that mathematics is remarkably robust.” There’s little danger, in other words, that the whole edifice of math could come crashing down.
That said, using Lean has also led to new math. In 2019, the mathematician Peter Scholze wrote a proof by hand of a theorem that was poised to play a key role in a new mathematical theory he was developing. But the proof was extremely complicated, and he struggled to determine if it was correct. So in late 2020, a team of mathematicians led by Johan Commelin and Adam Topaz set out to formalize the proof in Lean. Several months later, they confirmed that it was correct, giving mathematicians greater confidence in Scholze’s new theory. And in the process, they found a cleaner proof and refined some of Scholze’s original ideas.
“It forces you to think about mathematics in the right way,” said Kevin Buzzard, a mathematician at Imperial College London and one of Lean’s biggest proponents. “It forces you to become an artist.” (Buzzard has spent the past year working to use Lean to formalize a proof of Fermat’s Last Theorem, an important result whose proof is famously long and complicated.)
Courtesy of Kevin Buzzard
Moreover, taking the time to develop Lean now might be a good investment in a future where artificial intelligence is bound to play a bigger role in mathematics. As mathematicians try to use AI to write informal proofs, it will be more important to verify their accuracy using programs like Lean. (Plus, AI is already helping to write Lean proofs more efficiently.)
Still, the widespread adoption of Lean comes with risks. Could Lean, like Bourbaki, subtly shift the kinds of questions that mathematicians find interesting?
A ‘Moving, Shifting Beast’
Within Lean, there is little room for conceptual, methodological, or ideological diversity.
For one thing, every new proof in Lean can only use formal definitions and theorems that have already been verified and stored in its library. This means that these definitions and proofs need to seamlessly fit together. It also means that updating or changing a definition creates a domino effect: Proofs written with the old definition may not work with the new one.
That could be a problem. Mathematics is “not a fixed and finite and formalized enterprise,” said Stephanie Dick of Simon Fraser University. “It’s a moving, shifting beast, and the terms of it are changing all the time.”
Eric Sucar/University of Pennsylvania
Because of this, previous attempts to digitize mathematical results (such as a 1994 project called the QED Manifesto) quickly deteriorated into arguments about which definitions and frameworks to use. “Everybody loves this idea in principle, but in practice, it’s a nightmare,” Dick said. “They disagree about what programming language to write in. … There’s fundamental disagreement about whether this kind of project could be possible at all.”
To avoid these disagreements, a dedicated group of Lean users is responsible for determining which definitions should go into Lean’s library and how those definitions should be coded — much as Wikipedia does it, according to Simon DeDeo of Carnegie Mellon University.
“It is really a community trying to do the best thing for the community,” said Emily Riehl, a mathematician at Johns Hopkins University. So far, it’s worked, and the process has been largely democratic. But, she said, “what’s bad about it is, there is one decision that will be made in the end, [when] in many cases, there’s not one correct decision. Some people will be happy, and other people will be unhappy.”
Just as Bourbaki’s approach was optimal for certain subjects and not others, the Lean language and the choice of definitions that go into its library are better suited to some areas of math than others. They’re a good fit for number theory and algebraic geometry, for instance. Graph theory and category theory, not so much.
This is just one way Lean could make math more homogeneous. Dick points out that past technologies — even choices of which notation to use — have subtly changed how mathematicians approach their work. Lean might encourage them to focus on developing concepts that can be formalized more easily, even if they don’t realize it. “I’ve now found so many cases where something like that is happening,” she said — where “it actually shifts the focus and the intuition and the understanding away from the mathematical problem domain toward the behavior of this system.”
There is certainly a lot to be excited about when it comes to Lean. But Riehl, for her part, thinks that mathematicians should try to use more than one kind of proof assistant, rather than relying solely on Lean. She’s not sure how practical that will be, however, given how much effort formalization requires.
On Overcorrection
For centuries now, mathematicians have sought greater rigor by focusing on whether they can verify every line of a proof. But that wasn’t always the case. To Descartes in the 1600s, rigor meant being able to hold an idea in your head and intuitively understand why it’s true. As a result, according to Akshay Venkatesh of the Institute for Advanced Study, older proofs used to “have a kind of grittiness.”
“It doesn’t make for a formally elegant argument,” he said. But it’s “something a human being can easily understand.” Modern proofs are more elegant, sure. But they’re also more slippery, harder for the mind to get a grip on. (Interestingly, Buzzard used similar language while discussing his hopes for how Lean would influence proof-writing. “I want this argument to be a thing of beauty,” he said. “I want it to slip down the throat.”)
This trend reflects a notion that’s now taken for granted: that proof should lie at the heart of math. “There’s no question that the concept of proof is a fundamental part of mathematics,” Venkatesh said. But “where I think there should be a question is whether it should be the defining feature of mathematics.”
Formalization in Lean would continue this trend of prioritizing proof. But it’s not the only future that mathematicians are imagining. Researchers are encouraged to think “that the only way forward is to have papers be Lean-formalized,” Asok said. “I would argue another way is that we just take a step back and stop writing so much. But that’s antithetical to the incentives that are in place.”
It’s impossible to predict all the possible ways that formalization in Lean could impact mathematics. What’s clear from history is that math has a tendency to self-correct — and that the future of this next wave of formalization will be one we haven’t imagined yet.
Editor’s Note: Alex Kontorovich is a member of Quanta Magazine’s advisory board.