撰文 | 嘉伟

回顾刚刚过去的2023年，结出累累硕果的组合数学是最令世人瞩目的数学分支。在该领域里，全年中几乎每两个月便冒出一项令全球数学家叹为观止的重大理论突破。刚到10月份，今年在组合学方面的重要论文，竟然给研究和学习者一种“吃撑”的感觉：极值图论和拉姆齐理论、平面染色理论、平面密铺、不可传递骰子、加性组合以及被菲尔兹奖得主W. T. Gowers誉为组合学（可能的）第一猜想的“有限集合的并集猜想”，组合学中的各个子领域全面开花，统统取得了历史性的重大进展，甚至为有些课题画上了完美的句号！

其实在9月中，著名数学家陶哲轩刚刚结束了一项持续了近两年之久的、重要又艰辛的工作——彻底解答高维空间里的单瓷砖平移周期性覆盖的问题——一个关联数理逻辑（图灵机）和高维离散几何的难题。同时，陶哲轩公开表示，他打算用一个多月的时间来学习一种名为Lean的、特殊的形式化编程语言。所以，不少人都感到，组合学全年高潮迭起的剧情或许终将归于平静，起码到2024年之前都理应是如此。

谁知在11月13日，组合数学大师Gil Kalai突然宣布，有一支团队刚刚证明了加性组合学里的圣杯、已故的杰出女性数学家Kati Marton提出的著名猜想——多项式Freiman-Ruzsa猜想。

合著论文的团队，几乎是当前人类能拿出来的组合学最强阵容：W. T. Gowers、Ben Green、Freddie Manners、Terence Tao（即陶哲轩）。他们让过去的一年拥有了一个数学版童话故事般的结局。

四位作者渊源颇深。Gowers和陶哲轩，都是菲尔兹奖得主，是当代组合学界的领军人物。陶哲轩荣获菲尔兹奖的重要理由之一便是与Ben Green共同发现了Green-Tao定理。Freddie Manners则是Green的博士生，现为加州大学圣迭戈分校的数学副教授。 

随后一个月的时间里，陶哲轩等人又做了一件轰动数学界的大事：使用前文提到的Lean语言，把他们的证明形式化。它在数学史上的重要性或许还要超越证明猜想本身。 

编写Lean语言代码的时候，陶哲轩借助了当下流行的AI编程助手Copilot。因此，当相关新闻传回国内时，一些公众号误以为陶哲轩借助AI证明了重要的数学猜想，并诞生不少以此为标题的文章。

这种说法当然是错的。 

但是，为什么陶哲轩的团队用Lean语言形式化了论文就引发了学术界的巨震？为了方便理解，事情还得从“加性组合是什么”说起。

加性组合学（Additive Combinatorics）是一门非常年轻的数学分支。正因为年轻，它也是当前数学界最有活力的研究领域之一。 

它起源于一个国人非常熟悉的哥德巴赫猜想：

任一大于2的偶数都可写成两个质数之和。

从上面的哥德巴赫猜想，我们可以推得所谓的弱哥德巴赫猜想：

任一大于5的奇数都可写成三个质数之和。

在1742年普鲁士的数学家克里斯蒂安·哥德巴赫（Christian Goldbach）与大数学家莱昂哈德·欧拉（Leonhard Euler）通信之前，人们普遍认为，质数就是用于相乘的，而没人考虑过质数之间的加法会带来何种性质。

事实证明，哥德巴赫猜想是最难的一类问题。直至今日，数学家对于哥德巴赫猜想的完整证明仍然没有任何头绪。实际上，在猜想提出后的很长一段时间内甚至毫无进展，直到20世纪20年代，数学家才从组合学与解析数论两方面分别提出了解决的思路，并在其后的半个世纪里取得了一系列突破。

哥德巴赫猜想迫使数学家去考虑质数的加法结构，由此诞生了一门学科：加法数论。数学泰斗华罗庚则称它为堆垒数论！其中更偏组合学的研究路线如下：考虑全体奇质数构成的集合，令其与自身相加，如果得到的“和集”包含所有大于4的偶数，则猜想获证。

所谓集合相加，就是一个集合里的每一个元素，与另一集合里的每一个元素相加。其和构成的新集合叫和集。

我们以简单的有限集加法为例：

{1，2，3}+{1，2}={2，3，3，4，4，5}={2，3，4，5}（因为集合里重复的元素看成是同一个元素。）

从上面可以看出，这一路线更加偏整体和宏观，是往系统里“塞”结构。另一方面，解析数论里的筛法工具，则是把系统里的“多余”结构过滤掉。当然，这是一种大而化之的漫画式解读。实际上，两种研究风格是互相渗透，互相“利用”的。为了发展组合学方法，需要大量解析数论里的筛法技术。

虽然一开始，加法数论里的组合路线率先为哥德巴赫猜想带来了突破，苏联数学家列夫·根里霍维奇·施尼雷尔曼（Lev Genrikhovich Schnirelmann）借助上面集合相加的组合学思路（同时运用简单的筛法），证明了任何足够大的自然数，都可以写成若干质数之和。虽然这一结论离哥德巴赫猜想还有十万八千里，但这是第一次在自然数与质数和之间建立起关系，可以看作是从0到1的突破。

苏联著名的数学家亚历山大·雅科夫列维奇·辛钦（Aleksandr Yakovlevich Khinchin）将施尼雷尔曼的结论誉为“数论三大明珠”之一。辛钦就是《数学分析简明教程》《数学分析八讲》等经典教材的作者。学习概率论的朋友，对辛钦大数定律应该也不陌生。

遗憾的是，在数学实践中，尤其是陈景润发表了解析数论中著名的陈氏定理（“1+2”）之后，人们意识到，施尼雷尔曼的组合学路线并不是攻克哥德巴赫猜想的正确思路。因此迟至1960年左右，这类研究逐渐冷了下来。

幸好，传奇数学家保罗·埃尔德什（Paul Erdős）在这一领域里持续耕耘。后来陶哲轩等人从他手中接过接力棒，扛起加法数论与组合学的大旗。同时，其它几个数学领域里不断提出研究加法结构的需求，以及组合学的进步等因素共同作用，使源于加法数论的组合学思想，成长为独立的数学分支——加性组合学。虽然加性组合学或许不适于攻克哥德巴赫猜想，但它展示了广袤的研究前景，蕴藏着丰富的数学内容。 

多项式Freiman-Ruzsa猜想的证明，就是最新结出的甜美果实。遗憾的是，这个猜想是非常专业的数学内容，几乎无法用简单、清晰的方式解释给读者。这里仅能提供一种感性的理解思路。

关于集合的加法，有一个符合经验的直观洞见：如果集合A本身拥有很好的代数结构，则A+A的和集的规模（就是元素个数）与A相比，不会太“大”。

由这一观点出发，数学家Kati Marton应用逆向思维，提出如果A+A的和集足够小，则我们可以推知A所具有的代数结构。

把上面的思想用数学术语严格陈述，可以得到多项式Freiman-Ruzsa猜想：

Marton是出生于匈牙利的数学家，因其在信息论、concentration of measure（随机变量取值集中的现象）、概率论和遍历理论方面的研究而闻名于世。在对concentration of measure研究中，Marton巧妙地引入信息论和熵的概念，获得了一个简短的精彩证明。在多项式Freiman-Ruzsa猜想的证明中，类似于上面的熵方法似乎扮演了重要的角色，这一点真是再恰当不过了。 

另外值得一提的是，虽然多项式Freiman-Ruzsa猜想是限制在特征为2的有限域上的，但陶哲轩等人认为，他们的方法可以推广到所有的有限域上（具体论文将在未来发布）。也就是说，多项式Freiman-Ruzsa猜想在所有有限域上都是成立的。 

还记得前文提及，陶哲轩在去年9-10月期间宣布去学习名为Lean的语言吗？在他们把证明多项式Freiman-Ruzsa猜想的论文发布在预印本网站arXiv上几天后，陶哲轩立即着手进行证明的形式化工作——用他花了一个多月学习的Lean语言。 

Lean语言的“商标”是L∃∀N，∃是数理逻辑里表示“存在”的符号，∀则是表示“任意一个”的符号。Lean语言本身是一种函数式编程语言，同时也是定理证明器。它有一个包含已知定理的数据库Mathlib（目前尚未竣工）。如果把人类撰写的、符合人类阅读习惯的证明语句，转成形式化的机器语言——相当于得到了一个程序，再在电脑上运行该程序，则可以通过运行结果知道原本的证明是否成立！由包含逻辑漏洞和错误的证明转化的程序，在运行时会报错。

陶哲轩正是打算形式化自己团队的证明，把它转为可运行的程序以校验其正确与否。他以协作的方式展开了这个项目，利用在线软件源代码托管服务平台GitHub来统筹全球25位志愿者的工作。在此过程中，他们使用了名为Blueprint的管理工具。工具由巴黎萨克雷大学的数学家Patrick Massot开发。功能包括将陶哲轩所表达的“数学式英语”转换成计算机代码。Blueprint 还具备多种功能，其中之一就是创建一张图表，用以呈现证明中涉及的各种逻辑步骤。一旦这个图表中所有的气泡变成陶哲轩所形容的“可爱的绿色”，团队的工作就算完成了。

12月5日，Gowers宣布，关系对象图里的气泡框统统化为了绿色。这意味着，他们的证明经形式化和上机运行后，得以确认无误。

这件事或许会颠覆现有数学界的研究面貌。Lean技术开源社区最重要的推广者、伦敦帝国理工学院的Kevin Buzzard 表示：“从根本上来说，显而易见的是，当你将某些东西数字化时，你就可以以新的方式使用它。我们将把数学数字化，这会让数学变得更好。”

要知道，越是重要的论文，审稿时间则会越久。在现代数学史上，目前最重要的两篇论文分别是证明费马大定理那一篇和证明庞加莱猜想的那一篇。前者的总审稿时间长达2年，而后者更是经历了总时长7年的反复审查（因佩雷尔曼的证明过程过于简略）。

本文开头曾提及2023年有大量组合学方向上的突破性进展。其中针对拉姆齐问题的杰出论文公布于3月份，然而直到9月份，人工审稿仍未完成！

但是，陶哲轩等人的全新论文，其分量大致与3月份这篇相当。但在公布2周后，我们就已然可以确认，它是正确的。这意味着借助Lean语言形式化证明，可以节省大量的时间与人力成本。

如果再往深里思考：学术期刊的存在意义是什么？

一家好的期刊，可以提供权威性，而权威性又来自于期刊会审校自己刊发的论文，使论文的正确性有所保障。但人工审校的可靠性并不高。实际上，与机器辅助证明相比，人类犯错误的可能性是算法的1000倍。如果以Lean为代表的，可将数学证明形式化的编程语言被大规模使用，那数学期刊的存在意义就会被大幅削弱，甚至不再需要数学期刊。

让我们畅想一下未来。数学家只需把论文发布在网上（如arXiv等平台），后面附上论文形式化后得到的代码，其他人就可以轻易地验证论文里的证明是否正确无误，从而迅速接受或拒绝这篇论文。甚至以后用于传播和保存的正是代码本身，当我们阅读论文的时候，可以通过“反编译”手段，把代码转为人类可读的文字。从此，作为学术交流中枢的数学期刊将不再是必要的，而是成了某种学术收藏品的概念，同时因为审稿成本近乎为0，期刊的价格也应大幅降低。同时，书写习惯还会反过来作用于我们的思考方式。陶哲轩在形式化的工作结束之后表示：“我最近几天，每次想要表达的时候，潜意识里都会想着如何以一种更便于形式化的方式阐述和论证。”他不知道这会不会成为一种习惯，但乐于长期观察，看看语言方式对思维的影响。 

上面关于期刊的部分，绝非笔者个人一厢情愿的幻想。仔细考察当前数学界两位最活跃的领导者——陶哲轩与Gowers——对数学期刊的一贯态度，就能窥探到他们所乐见并亲力推动的未来。

他们一贯支持开源和公平的学术出版模式，反对商业出版社的垄断和高昂的订阅费用。他们倡导论文开源的理念，认为学术成果应该免费地分享给所有的读者。

陶哲轩和Gowers在2012年还曾发起针对商业出版社Elsevier的抵制运动，号召数学家不要向Elsevier旗下的期刊投稿、审稿或编辑，也不要购买或阅读Elsevier的期刊。他们支持开源期刊的发展。开源期刊通常采用开放获取的许可协议，允许读者自由地下载、复制、分发、引用、修改和使用期刊上的文章。陶哲轩和Gowers还是一些开源期刊的创始人。

读到这里，大家应该也猜到了，陶哲轩与Gowers这一次把自己的证明形式化，绝非一时心血来潮，而是一次有预谋的无声呼吁：他们认为这是一个时代的契机——去商业学术期刊化的契机。AI浪潮席卷而过，为他们冲刷出另一条学术交流之路。

总而言之，在未来，数学界内部的交流方式，新定理的认可速度，论文的写作和获取方式，数学证明的表达规范，都将与现在不同。

当然这也和数学自身和数学证明的特性有关。诸如历史这样的学科，或者实验性的学科，是无法把论文形式化的。

或许，抗拒这一潮流的唯一内源性力量是，形式化论文本质上是把部分审稿成本转移到论文作者的身上——我们为了向学界“自证”，就需要再掌握一门编程语言Lean（或未来取代它的语言），并且要花时间形式化自己的数学论文。但是，在2022年以后，似乎学习使用新的编程语言不再是什么沉重的负担。因为大语言模型的出现，现有AI在其它方面或许帮助有限，但是在辅助编程方面，则可以带来极高的增益。而随着相关技术的进步。这种AI助手只会越来越强。同时，相关语言，如Lean也会迭代得更加灵活，方便。 

未来的发展，无论是计算机辅助证明工具，还是各类型的AI，最终目标都是对数学定理的自动化证明。现在的Lean本质上还是一种传统的计算机辅助证明工具，其核心是形式化证明。它不是当前主流的生成式AI和CoT（思维链）可自动推理的大语言模型。形式化证明的概念已经存在很久了，与基于大模型和生成式方法的当前人工智能是完全不同的概念。当然，即便是后者，目前也无法独立完成真正意义上的数学证明。在将Lean语言与AI结合的过程中，除非有一天AI能够创造性地自动完成Blueprint和Lean中的关键创造性步骤，否则我们也无法将这种工具称为具备数学能力的人工智能。 

未来有太多的可能性，而现在局势已然明了的部分则是，Lean或某个取代它的后继语言，代表着数学研究与论文写作的未来。

Lean的最新版本是Lean 4。它的目标是提供一个高效、可扩展、可靠的平台，用于形式化数学、验证软件和硬件，以及开发通用的函数式程序。我在这里分享一本开源教程Mathematics in Lean（链接见参考资料6）。

2. Marton’s “Polynomial Freiman-Ruzsa” Conjecture was Settled by Tim Gowers, Ben Green, Freddie Manners and Terry Tao ‹ Combinatorics and more ‹ Reader — WordPress.com

3. Additive Combinatorics | Van Vu (yale.edu)

4. On a conjecture of Marton | What's new (wordpress.com)

5. ‘A-Team’ of Math Proves a Critical Link Between Addition and Sets | Quanta Magazine

6. Mathematics in Lean (leanprover-community.github.io)：https://leanprover-community.github.io/mathematics_in_lean/mathematics_in_lean.pdf