你以为学数学就是画几何图、会算术能数数？幼稚了

解读科普顶级期刊《量子杂志》这篇有关数学与形式的文章：

你可能会觉得，数学嘛，不就是算算数，证明个东西，对就是对错就是错。但你不知道，数学家这群强迫症晚期患者，为了“严谨”两个字，已经折腾了好几百年。
他们就像一群有洁癖的处女座，看哪都觉得不够干净。

最近，这帮人搞出了一个大招，要用一个叫Lean的电脑程序，把全宇宙的数学定理都变成电脑能读的代码，然后让电脑来当裁判，证明你这步推那步到底行不行。
听起来是不是很酷？但问题来了，这样做会不会严谨到变态，反而把数学本身给玩坏了？
别急，咱们从古希腊那个叫欧几里得的老哥开始，一路笑喷着聊到今天数学系的走廊里，教授们是怎么为了这事儿差点打起来的。

咱们先回到古希腊。欧几里得当时就琢磨，如果大家能同意几条最基本的规则，比如“两点之间线段最短”这种，那咱们就可以用逻辑推理，像搭积木一样，搭出无数新的数学真理。
这想法牛不牛？牛！但是，问题出在执行上。

早期的证明，虽然号称是纯逻辑，但里面经常藏着一些没说出来的“潜规则”，或者靠直觉蒙混过关。
这就好比你说“因为小明是我兄弟，所以我的钱就是他的钱”。听起来好像挺有道理，但你忘了说“我们俩是拜把子的兄弟，而且我脑子进水了”（这是隐藏的假设、上下文语境Context）。

所以，那些古老的证明里，经常有小漏洞像地雷一样埋着。
你看着是那么回事，但真较真起来，心里就发虚：“我到底能不能拍着胸脯说这绝对没错？”
数学家不干啊，他们追求的是绝对真理，怎么能容忍这种“好像对”的感觉？

于是，从几百年前开始，这帮数学家就踏上了填坑之旅。

到了20世纪初，他们终于把自己要用哪些基本规则（也就是公理）给定下来了。然后还不放心，又搞出了各种逻辑系统和标准，要把自己的论证“形式化”。

什么叫形式化？就是把你每一步推理都掰开了揉碎了，写到最最最啰嗦的程度，确保不管你的证明有多长、有多绕，结论都必须是铁板钉钉的真。

这就像你教一个智商为零的机器人走路。你不能说“走过去”，你得说“抬起右脚，向前移动5厘米，放下；抬起左脚，向前移动5厘米，放下”。每个动作都得拆成最细的指令，这样才能保证机器人绝对不摔倒。数学家就是要把自己的证明写成这种“机器人说明书”，累不累？累死了。但这让他们心里踏实啊，感觉自己的知识大厦是建在花岗岩上，而不是沙滩上。

这种追求形式化的努力，确实带来了信任。

但它的功劳远不止于此。这股形式化的浪潮，阴差阳错地帮数学家们发现了不同数学领域之间那些八竿子打不着的神奇联系。就像你本来在研究怎么切蛋糕，结果发现这原理竟然能用在发射火箭上。它还带着数学拐进了很多意想不到的新胡同，开拓了新天地。

明尼苏达州马卡莱斯特学院的大卫·布莱索德老师说，这个过程教会了我们一个道理：“你经常不知道自己不知道什么。得学会谦虚。”这话说得多好！你觉得自己懂了，但一较真，发现全是坑。

但是，数学要想有大进展，就必须有大胆的想法。而这些大胆的想法，通常来自实验、直觉，来自在你根本没法证明每一步都合乎逻辑的情况下，就去探索全新的数学世界，去瞎试新理论。这是一种不那么形式化的玩法，一开始往往错漏百出。
这就像你想发明一个新菜，你不能先把营养学、分子料理理论全部学完，然后再做。你得先凭感觉往里扔盐、扔辣椒，尝尝味道，不行再改。
数学家也一样，他们得先有“灵光一闪”，然后再回过头去补证明。

所以，怎么在“天马行空的创造力”和“吹毛求疵的严谨性”之间找到平衡，就成了一个世纪难题！
有时候，形式化一过头，就把这种平衡给砸了：
在有些数学家看来，形式化是走向更确定、更可靠的未来；
但在另一些数学家眼里，这就是“杠精”行为，是给进步使绊子。

你觉得呢？

极限的诞生：数学家如何被“奇怪曲线”逼疯的

好了，历史课继续。

咱们来讲讲那个著名的“严谨化”里程碑事件。这事儿得从微积分说起。17世纪末，牛顿和莱布尼茨这俩哥们儿（也是老冤家）各自捣鼓出了微积分。

微积分是干嘛的？就是研究一个函数在某个点上变化有多快。但你知道吗，微积分的思想其实已经在地球上晃悠了好几千年。
早在公元前3世纪，阿基米德那老哥就在干类似的事儿了。他想算圆的面积，就先研究那些有直边的形状，比如多边形。
他发现，如果你用的多边形边数越来越多，它的面积就越来越接近圆的面积。这就是在估算一个“极限”。
牛顿和莱布尼茨就是把“极限”这个工具拿来研究变化率，于是微积分就诞生了。

微积分一出来，立刻在数学和物理界成了香饽饽，哪儿都能用。但是，用现代的标准看，它一点都不“形式化”。牛顿和莱布尼茨的论文里，很多地方含糊其辞。微积分这玩意儿离不开“无穷”和“无穷小量”的概念。

啥是无穷小？就是比任何你能想到的数都小，但又不是零。听起来就很玄乎对吧？牛顿和莱布尼茨就用模糊的几何语言来描述这些概念。这就导致一个问题：如果你用错了公式，可能会算出很荒谬的结果，比如除以零这种低级错误。这就好比你开跑车，爽是爽，但刹车不灵，随时可能翻车。

神奇的是，在长达150年的时间里，竟然没人觉得这是个问题！（宗教几千年，掉入陷阱的人也没觉得自己信仰的有啥问题，身在庐山不识庐山！）

科学家们靠着经验和直觉，知道什么时候用微积分管用，什么时候用会翻车，就这么将就着用。
就像一个老司机，虽然车有点毛病，但他知道哪个档位不好使，照样开得飞快。

但是到了19世纪初，情况变了。

数学家们开始遇到一些怪胎，比如无穷级数（把无穷多个数加起来）和一些奇奇怪怪的、到处是尖角的曲线。这些玩意儿完全违背了他们的直觉。他们以前觉得“显然”正确的东西，在这些怪物面前全都不好使了。

这下子，数学家们慌了。

这种恐慌不是孤立的。当时整个艺术界和科学界都在大反思！哲学家、画家、作家、科学家都开始质疑自己知识的根基：

哥伦比亚大学的历史学家阿尔玛·斯坦加特说：“直觉变得可疑了。大家都觉得，直觉可能会把你带沟里去。” 对，你脑袋里那个“我觉得应该是这样”的声音，突然就不靠谱了。所以，数学家们觉得，必须得做点什么了。

于是，一批大牛数学家，比如尼尔斯·阿贝尔、奥古斯丁-路易·柯西、卡尔·魏尔斯特拉斯，他们意识到，要想搞明白那些奇怪的无穷和曲线，就得回到最原始的定义。

他们开始问一些基础到让人崩溃的问题：到底什么是函数？
函数“连续”是什么意思？
把无穷多个东西加起来，到底会发生什么？

这些问题听起来像不像哲学？
但数学家们硬是给出了“形式化”的定义，把这些概念给锁死了。

比如魏尔斯特拉斯，他就给出了我们现在还在用的那个“极限”的精确数学定义。这套新定义，让数学家们能够以前所未有的深度和严谨性去研究函数，最终催生了一个全新的数学分支——“分析学”。

今天，分析学是数学里最重要的领域之一。从流体流动、电流，到遥远恒星的化学成分，分析学都能插上一脚。而且它跟其他几乎所有数学领域都紧密相连，包括更古老的数论和几何。

所以你看，形式化微积分，竟然长出了一棵参天大树。

另外，这事儿还顺便催生了“集合论”，就是给现代数学制定底层规则的。现在集合论自己也成了一个热门研究领域。
你看，一个强迫症行为，竟然带来了这么大的好处。

当然，也不是所有人都为形式化欢呼。
物理学家奥利弗·海维赛德在1899年就吐槽说：“当严谨主义者那些湿毯子把你的热情人工冷却之后，你很难再嗨起来。”
这话说得太形象了。
你正热血沸腾地想搞个大发现，结果旁边有人一直说“不对，你这个步骤不严谨”，就像冬天有人往你头上泼冷水。

历史学家杰斯佩·吕岑在回顾那个时代时写道：“分析学获得了严谨性和普适性，但失去了优雅和简洁，并且与直觉疏远了。许多数学家对这种趋势感到遗憾，但又难以逃脱。” 翻译一下就是：我们证明了更多东西，但证明过程变得又臭又长，一点美感都没有了，而且跟我们的直觉完全不搭界。很多数学家觉得这很可惜，但又没办法，因为你不严谨就会出错。

不过，有趣的是，严谨派和反严谨派最终找到了一个折中方案。

数学家们继续使用柯西和魏尔斯特拉斯那些精确到变态的定义，但他们同时也开发出了一些框架，让海维赛德这样的科学家可以更自由地使用无穷和无穷小进行计算，而不必每一步都严格遵守那些条条框框。

换句话说，你没那么严谨，我也不打死你，但我知道你那个不严谨的玩法背后，其实是可以用严谨的方式解释的。

这就是一种默契。所以，形式化不是他们唯一的目标。

其实这个故事里有个关键点：形式化的“意图”很重要。

魏尔斯特拉斯和他的同事们当初是为了解决特定问题（那些奇怪的函数行为），才求助于形式化。他们是有的放矢。然后分析学、集合论这些形式化系统，是自然而然生长出来的，而不是为了形式化而形式化。

大数学家大卫·希尔伯特在1905年就写过一段很妙的话：“科学大厦的建造不像盖房子，不能先把地基打得牢牢的，然后再去盖房间。相反，科学家应该先找到‘可以闲逛的舒适空间’，然后，当地基不牢的迹象出现，无法支撑房间扩建时，再去加固它们。”

他说：“这不是弱点，而是正确且健康的发展路径。” 说白了，形式化是为了解决问题，而不是为了装逼。如果为了形式化而形式化，那后果可能就完全不一样了。

布尔巴基的“冷宫”：当数学变得像禁欲系男神

好，讲完微积分的故事，咱们来看看一个把“形式化”玩到极致的组织，一个叫“布尔巴基”的数学家秘密社团。这个社团的哲学思想，可以说是数学史上最著名（或者说最臭名昭著，看你怎么想了）的流派之一。

故事回到20世纪30年代中期的法国。当时法国的数学已经衰了几十年了。一战让法国损失了一整代有才华的学生和研究者。大学里的数学教学方式也是各自为政，支离破碎，用的教材都老掉牙了。于是，几个年轻数学家就凑在一起，搞了个秘密社团，取名“布尔巴基”。

他们一开始的目标还挺谦虚：写一本更连贯、更现代的新教科书，把法国数学课程带入20世纪。
但是，这帮人的野心很快就膨胀了。

到今天，布尔巴基（其成员身份至今保密）已经出版了40多卷著作，几乎覆盖了数学的所有领域。
牛不牛？真牛。
但这些书的真正遗产，不是内容，而是风格。

布尔巴基把抽象性置于一切之上。他们拒绝具体的例子和计算，只追求最最最普遍的陈述。他们呈现每个证明，就是一系列逻辑推理，通常完全不提任何背后的直觉或理由。就像你拿到一本菜谱，上面写着“步骤1：将物质A与物质B在特定条件下结合”，但就是不告诉你A是鸡蛋，B是面粉，特定条件是“搅拌”。你看得懂吗？能看懂，但你想摔书吗？绝对想。

以色列特拉维夫大学的历史学家利奥·科里说：“这是一种非常形式化的风格，非常朴素，非常苦行。”
布尔巴基的哲学思想迅速传播开来，几乎影响了全世界的数学。

巴黎萨克雷大学的帕特里克·马索说：“它的影响是巨大的。最成功的部分已经如此深入地融入了通用的数学知识和风格，以至于你很难想象之前是什么样了。” 就是说，我们现在觉得理所当然的很多数学写法，其实都是布尔巴基当年定下的规矩。数学因此变得滴水不漏，但也越来越抽象，越来越难懂。《为了科学》杂志的长期编辑、布尔巴基传记作者莫里斯·马沙尔写道：“从教学的角度来看，这不是一个明智的决定。” 但布尔巴基对抽象化的强调，深刻地塑造了数学研究，其影响好坏参半。

有些数学家非常崇拜布尔巴基。马索就认为，通过抽象和优雅，“你被迫去理解真正让事物运作的是什么，而哪些只是噪音。” 在他们看来，形式化带来了清晰。但是，布尔巴基的项目也带来了意想不到的后果。他们的词汇和风格，并不是适合所有类型的数学。

比如说，“组合学”（研究计数的科学）和“图论”（研究网络关系的科学）这些领域，通常非常具体、非常可视化，需要画图、需要举例子。那么，毫不意外，在布尔巴基思想统治下的几十年里，组合学和图论在美国和欧洲大部分顶尖学府里都被边缘化了。它们只能在那些布尔巴基影响力较弱的地方（比如匈牙利）才能茁壮成长。

剑桥大学的贝拉·博洛巴斯说：“图论曾经是拓扑学的贫民窟。这种氛围直到最近才改变，非常非常最近。”
想象一下，一个很有才华的年轻数学家，因为喜欢画图、喜欢数数，就被主流学界鄙视，说他搞的不是“真正的数学”。这多冤啊！

即使在那些在布尔巴基框架下蓬勃发展的领域（比如代数、拓扑、分析），也有些数学家担心布尔巴基“太成功了”。他们认为，证明的写法、理论的构建方式，都变得过于同质化，千篇一律。南加州大学的阿拉文德·阿索克说：“感觉它减少了数学的文化多样性。”

在布尔巴基之前，比如代数几何这个领域，有很多不同的版本。
在法国，方法建立在分析学基础上；
在意大利，则是一种几何风格占据主导。意大利学派虽然不够严谨，包含很多错误，但随着布尔巴基的影响力扩大，它很快就消失了。

当然，代数几何变得更可靠了。但是，通过切断其他可能的发展路径，布尔巴基带来了一个新问题。
阿索克说：“我不想要任何一种模式主导一切的数学。数学有一种值得保存的文化历史。” 你想想，如果全世界只有一个菜系，只有一种口味的汉堡，那世界得多无聊？数学也一样。如果大家都只按一种风格做研究，很多有趣的、有创造性的想法就会被扼杀在摇篮里。

所以，布尔巴基的故事告诉我们，追求严谨和形式化，如果不加节制，可能会变成一种思想上的霸权，排挤掉那些不那么“酷”、不那么“抽象”的领域和风格。这就是为什么，当今天我们面对Lean这个更强大的形式化工具时，数学家们会如此警惕。他们怕历史重演，怕Lean成为新时代的布尔巴基，把数学再次推入一个冰冷的、缺乏多样性的“冷宫”。

Lean的“封神榜”：把数学变成乐高积木

好，现在终于要说到今天的重头戏了，那个叫Lean的电脑程序。

尽管布尔巴基、柯西和魏尔斯特拉斯做出了最大努力，但真正形式化的证明一直只是理论上的存在，在实际操作中几乎没人会去写一个完全形式化的证明。
为什么？
因为太TM累了。
你写一个“1+1=2”，得先定义什么是“1”，什么是“加法”，什么是“等于”，什么是“2”，然后一步步证明。
数学家是人，不是机器。但现在，有些数学家希望电脑能改变这一切。

从上世纪60年代开始，研究者们就一直在开发一种叫“证明助手”的电脑程序。用证明助手，数学家把证明的每一行（包括每一个定义）都用电脑能懂的语言写出来，然后证明助手会检查逻辑。哪怕只有一个步骤没有从前一步推导出来，比如你没有严谨地证明“1+1=2”这个事实，程序就不会认为你的证明是正确的。想象一下，你写作业，老师变成一个AI，你的每一个等号、每一个因为所以，都必须符合最严格的逻辑规范，否则就判错。这就是Lean在做的事情。

目前，数学家们正希望用Lean这个证明助手，把整个数学都形式化。

他们已经建立了一个包含超过12万个定义的库，并验证了25万个定理。有好几个数学家全职维护这个数据库，保持更新，审核新贡献。他们还获得了超过1000万美元的资助，大部分来自一位亿万富翁金融家。

这投入，不可谓不大。罗格斯大学的亚历克斯·康托罗维奇说，Lean是“革命性的”。
原因之一是，它把一个庞大的证明拆分成很多小块，每个小块可以独立处理、独立验证，然后还能在其他证明中重复使用。

他说：“想象一下，每次你想造一艘宇宙飞船，每个工程师都必须理解每一个部件——从开采铁矿石，到冶炼，到设计。现在有了这些形式化系统，你第一次可以像从货架上买东西一样，直接买别人做好的部件。” 这就像你玩乐高，不需要自己去开模做积木，直接拿现成的拼就行了。

Lean提供了标准化的、经过验证的“数学积木”。

但是，事情总有两面性。

用Lean来写和验证定义及证明，通常需要好几个月。（有的情况只需要几周，有的则需要一年多。）因此，有些数学家担心，他们的时间和资源花在这上面不值得。他们觉得，虽然验证证明很重要，但手工检查几百年来也运转得挺好。阿索克说，尽管“文献中有很多很多错误，但我的经验是，数学是极其稳健的。” 换句话说，整个数学大厦不太可能因为一两个没被发现的漏洞就轰然倒塌。你没必要为了那百万分之一的可能性，付出百倍的努力。

不过，使用Lean也确实催生了新的数学。

我给你讲个真事儿。2019年，数学家彼得·舒尔茨手动证明了一个定理，这个定理将在他正在发展的一个新数学理论中扮演关键角色。但这个证明极其复杂，连舒尔茨本人都搞不清楚到底对不对。

于是，2020年底，一个由约翰·科梅林和亚当·托帕兹领导的数学家团队，开始用Lean把这个证明形式化。几个月后，他们确认这个证明是正确的。这不仅让数学家们对舒尔茨的新理论更有信心，而且在这个过程中，他们还找到了一个更简洁的证明，并完善了舒尔茨的一些原始想法。

伦敦帝国理工学院的数学家、Lean的头号粉丝凯文·巴扎德说：“它迫使你以正确的方式思考数学。它迫使你成为一名艺术家。” 巴扎德在过去一年里，一直在用Lean把费马大定理的证明形式化。费马大定理可是数学史上最著名的结果之一，其证明以冗长和复杂而闻名。他说：“我希望这个论证能成为一件美丽的东西。我希望它能顺利地滑进喉咙。” 你看，他用了“美”这个词。在极致的形式化中，他找到了一种艺术感。

而且，现在花时间发展Lean，可能是一项面向未来的投资。未来，人工智能肯定会在数学中扮演更重要的角色。当数学家试图用AI来写非形式化的证明时，用Lean这样的程序来验证它们的准确性就变得更加重要了。另外，AI也已经在帮助更高效地写Lean证明了。所以，这不是一个孤立的技术，而是未来数学研究基础设施的一部分。

当“唯一”成为规则：Lean会扼杀数学的多样性吗？

尽管Lean有这么多好处，但它的广泛使用也伴随着风险。就像当年的布尔巴基一样，Lean会不会也悄悄地改变数学家们觉得“有趣”的问题类型？会不会让数学变得更加同质化？

首先，在Lean内部，几乎没有概念、方法论或意识形态多样性的空间。
因为，每一个用Lean写的新证明，只能使用已经验证并存储在库中的形式化定义和定理。这意味着，这些定义和证明必须能无缝地拼在一起。
这也意味着，更新或改变一个定义会产生多米诺骨牌效应：用旧定义写的证明，可能无法用新定义验证。这就像你房子的地基，一旦打好了，想挪动一块砖，整个房子都可能塌掉。这可能会带来问题。

西蒙弗雷泽大学的斯蒂芬妮·迪克说，数学“不是一个固定的、有限的、形式化的事业。它是一个移动的、不断变化的野兽，它的术语一直在变化。” 数学是活的，是演化的。今天你觉得完美的定义，明天可能就不够用了。但Lean的库一旦确定，就很难改动。

正因为如此，以前那些想把数学结果数字化的尝试（比如1994年的QED宣言项目），很快就因为大家争论该用哪些定义和框架而陷入僵局。迪克说：“原则上每个人都喜欢这个想法，但实践中，这是一场噩梦。他们不同意使用哪种编程语言……对于这种项目是否可能实现，存在根本性的分歧。”

为了避开这些分歧，一个专门的Lean用户小组负责决定哪些定义应该进入Lean的库，以及这些定义应该如何编码。
这有点像维基百科的模式，但又有不同。

约翰霍普金斯大学的数学家艾米丽·里尔说：“这真的是一个社群在为社群做最好的事。” 到目前为止，这种模式是有效的，过程也基本是民主的。但她同时指出：“不好的是，最终只会做出一个决定，而在很多情况下，并没有唯一正确的决定。有些人会高兴，另一些人则会不高兴。” 就像在岔路口，你必须选择一条路走，但两条路可能都通向罗马。选择了一条，就意味着放弃了另一条路上的风景。

就像布尔巴基的方法最适合某些学科而不适合其他学科一样，Lean的语言及其库中选择的定义，也更适合某些数学领域。它们非常适合数论和代数几何。但对于图论和范畴论，就不是那么回事了。这就会导致一种无形的引导：研究者可能会不自觉地倾向于选择那些更容易用Lean形式化的课题，因为这样“省事”。

迪克指出，过去的技术——甚至包括符号的选择——都已经微妙地改变了数学家的工作方式。

Lean可能会鼓励他们专注于那些更容易形式化的概念，即使他们自己没有意识到。她说：“我现在已经发现了很多这样的案例，它实际上把焦点、直觉和理解，从数学问题领域转移到了这个系统的行为上。” 你本来是想研究一个深刻的数学现象，但最后你花了很多时间去琢磨“怎么把这个现象喂给Lean吃”。这就像你本来想写一篇感人的小说，结果最后你一直在纠结“这个标点符号在Word里会不会显示错误”。工具反而成了主角，这难道不是本末倒置吗？

当然，对于Lean，我们有很多值得兴奋的地方。但里尔认为，数学家应该尝试使用多种证明助手，而不是只依赖Lean。然而，考虑到形式化需要付出的巨大努力，她也不确定这在实践中是否可行。毕竟，学会一个Lean已经够累的了，谁还有精力去学第二个、第三个呢？这就形成了一种“赢家通吃”的局面。一旦Lean占据了主导地位，其他可能性就会被挤压。

矫枉过正？数学的“证明狂魔”时代

几个世纪以来，数学家们一直在追求更大的严谨性，焦点都放在“能否验证证明的每一行”上。

但这并不总是如此。在17世纪的笛卡尔看来，严谨意味着能够把一个想法放在脑子里，并凭直觉理解它为什么是真的。因此，据普林斯顿高等研究院的阿克沙伊·文卡泰什说，古老的证明“有一种粗糙感”。“它不是一个形式优雅的论证，” 他说，“但它是一个人类可以轻松理解的东西。”

现代的证明更优雅了，这是肯定的。但它们也更滑溜了，却更难以让人的思维抓住了。

有趣的是，巴扎德在讨论他对Lean的期望时，用了类似的语言。他说：“我希望这个论证能成为一件美丽的东西。我希望它能顺利地滑进喉咙。”
现代的、形式化的证明，追求的是那种“滑溜溜”的顺畅感，但代价可能是牺牲了人类直觉的可触及性。

这种趋势反映了一个现在被认为理所当然的观念：证明应该处于数学的核心。
文卡泰什说：“毫无疑问，证明的概念是数学的基本组成部分。但我认为，应该被质疑的是，它是否应该成为数学的定义性特征。” 这是一个灵魂拷问。
数学到底是“关于证明的科学”，还是“关于模式、结构、直觉和发现的科学”？
证明是工具，还是目的？

用Lean进行形式化，会延续这种优先考虑证明的趋势。但这并不是数学家们正在想象的唯一未来。阿索克说，研究者们被鼓励去认为“唯一的出路是让论文被Lean形式化”。但他认为：“另一种方式是，我们只是退后一步，停止写那么多东西。但这与现有的激励机制是对立的。” 现在的学术圈，鼓励你多发论文，多出成果。写Lean证明虽然慢，但能发好期刊啊。你停下来思考，反而被认为是不务正业。所以，这个系统本身就在推动形式化的发展。

我们无法预测Lean的形式化可能以所有可能的方式影响数学。但从历史上看，数学有一种自我修正的趋势——而下一波形式化的未来，可能是我们目前还无法想象的。

也许，就像微积分的故事一样，我们会找到一个平衡点：用Lean来验证那些最关键的、最复杂的部分，同时保留非形式化的、充满直觉的、甚至有些“粗糙”的探索空间。也许，会出现多种证明助手，每种服务于不同的数学文化和风格。

也许，AI会帮我们自动把非形式化的证明翻译成Lean代码，从而大大降低成本。

但无论如何，有一点是肯定的：数学家们又开始了新一轮的折腾。他们一边喊着“严谨万岁”，一边又怕“严谨死了”。