陶哲轩用 AI 证明数学猜想实乃误读，但数学界仍大受震动

luyuanhong

陶哲轩用 AI 证明数学猜想实乃误读，但数学界仍大受震动

2023 年是数学界浓墨重彩的一年。组合学领域的知识爆发式增长。在去年年末，4 位重量级数学家更是组队拿下了加性组合学的圣杯。但对于加性组合学这一年轻、活力四射的研究领域，公众却知之甚少。而此事的后续，或许才是影响最为深远的。“我们将把数学数字化，这会让数学变得更好”。

撰文 | 嘉伟

回顾刚刚过去的 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 的博士生，现为加州大学圣迭戈分校的数学副教授。


图中人物从上到下，从左至右分别为 Gowers ，陶哲轩，Manners和Green 。|图源：Gil Kalai 的博客 Combinatorics and more: Image (wordpress.com)

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

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

这种说法当然是错的。

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

加性组合与多项式 Freiman-Ruzsa 猜想

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

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

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

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

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

如果 A 是一个特征为 2 的有限域 F 的子集，满足 |A+A|≤K|A| ，其中 K 是一个常数，那么可通过域上一个不大于 A 的子群的不超过 2*K^12 个陪集而将 A 覆盖于其中（原猜想表述里指数为未知常数，12 由最新论文所确定）。陪集的数量很可能非常大。但这是 K 的多项式，不至于随 K 的增大而指数级增长。


Kati Marton 悬挂在布达佩斯 Renyi 学院走廊上的照片。|图源：Gil Kalai的博客Combinatorics and more: Image (wordpress.com)

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

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

陶哲轩到底用 AI 做了什么？

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

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

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


12 月 4 日时还剩下一个小定理（图中蓝色对象框）未被形式化。|图源：teorth.github.io/pfr/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）。

参考资料

1. [2311.05762] On a conjecture of Marton (arxiv.org)

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.git ... ematics_in_lean.pdf

原创 嘉伟 返朴 2024-01-10 08:01 发表于北京

ysr

哥德巴赫猜想没有啥难的，小学生都可以看懂下面这个证明：

重生888@

中国网眼筛子，是哥德巴赫猜想的基础！基于这种筛子，导出0+0理论的四个公式，目前已获四项成果：
1. 任一大于等于30的 偶数，其素数对大于等于2；
2. 确定充分大的偶数（10^16）哥猜素数对范围；
3，用0+0理论证明哥猜1+1不成立，哥猜1+2 必定成立，不用一麻袋废纸！
4. 哥猜成立，必定是0+0=1（1个素数+一个素数=一个素数对）

ysr

准备投稿《现代教育进展》期刊的压缩后的文档（已经压缩到4341字，要求是4500字原来是6616字）：

白新岭

数学家们先入为主，打不破已有的条条框框。是，哥德巴赫猜想与组合学，数论，集合，群论，映射，微积分等等有着千丝万缕的联系，如何把它们零活的运用到哥德巴赫猜想中，是当前的难题。（我只所以，没有提到解析数论，复变函数论，是因为我对那些一窍不通）。

孪生素数对        0        2                内部合成        1        -1                相对距离        统计2
中项置零        -1        1                1        2        0                2        1
求其逆元        1        -1                -1        0        -2                0        2
                                                                -2        1
统计函数COUNTIF(F$2:G$3,I2)                                运算符号        a+b                        合计        4
这只是对孪生素数对的中项和合成的一个初步的内部合成结果的分析。

ysr

已经被证明的定理就是客观规律，就等于是客观事实，即使放在那里几百年也是不会改变的。再说不可能就没意思了。
我的证明虽然没有发表(我已经整理成书自费出版了一本《数论探秘》)，没有得到专家的承认，但事实不会改变，定理就是客观的事实，总有一天人类会明白这个道理，而把这个简单的东西当成世界级难题到那个时候就会觉得可笑了。真理不能发表是可悲的，不能让“后人复哀后人矣”。
当然，如果你对别人的证明有疑点是可以质疑的，如果发现了证明有错误，你是可以用事实和严格的逻辑推理来反驳和推翻的，但是不能用猜想去反驳。那你自己倒是可笑的，尤其人家“专门家”承认的东西，比如陶哲轩证明的那个东西。当然我也不知道他的证明过程对不对，结论是对的，那个东西初等数学就可以证明的。
张益唐的关于孪生素数猜想的证明我也没有见到，那个结论是对的，证明过程对不对咱也不知道，咱也不管他。孪生素数猜想并不难，我已经证明了，那就是个定理了。吹半天也没有用，不过在我眼里他那个东西没有价值。
我已经证明差为2，4，6，……，2n的素数对，都是无穷多的。
孪生素数对就是差为2的素数对，所以，孪生素数对是无穷多的，孪生素数猜想就是成立的。猜想内容就是说是孪生素数是无穷多的。张益唐说的差为7000万内的素数对可以有无穷多，在我这儿没有意义，没有价值。管他啥方法呢，方法越高级理论越高等越可笑了。
这个是我发在头条新闻上的评论，有人点赞回复了，转发一下吧！