AI改变数学

▲ 表面上看，数学这门人类最古老的学科，似乎自诞生之初就没有变化，现在的数学家仍然像两千多年前的阿基米德一样，主要靠纸笔演算的方式来进行研究。但实际上，数学家们对于新兴技术的出现，一直持开放态度。（农健/插画）

文｜左力

责任编辑｜王江涛

2026年5月20日，OpenAI官方宣布：其内部一个通用AI推理模型，自主证伪了一个埃尔德什难题“平面单位距离猜想”（Erdős Unit Distance Problem）。英国数学家、菲尔兹奖得主蒂莫西·高尔斯（Timothy Gowers）称之为“AI数学的里程碑”。为了表达他的震惊，他发帖说道：“如果你是一名数学家，那么在继续阅读之前，你可能需要确保自己已经坐稳了。”

而就在不久前的5月8日，高尔斯就在个人博客上发布了他最近使用GPT-5.5Pro的体验。在博文中，高尔斯写道：“在我几乎不进行专业指引的情况下，GPT-5.5Pro仅用了一个小时，就完成了一项具有数学博士研究水准的成果。”

稍早之前的4月，北京大学北京国际数学研究中心AI4Math团队的董彬和刘若川、肖梁等人宣布：他们构建的自动化AI框架解决了交换代数中的安德森（Anderson）猜想，并在定理证明器Lean4中完成了形式化验证。

更早时候的2月，Math,Inc.公司宣称，他们研发的人工智能系统高斯（Gauss），完成了8维和24维最佳球堆积问题的解答的形式化验证。这一解答原由乌克兰女数学家马林娜·维亚佐夫斯卡（Maryna Viazovska）及其合作者于2016年给出，维亚佐夫斯卡也因此获得了2022年的菲尔兹奖。这也是第一项由AI形式化验证的菲尔兹奖级别的数学成果。

这一系列的事件表明，AI正在改变数学这门古老的学科，以及数学家们的工作方式。

一直以来，数学界普遍采用同行评议的机制，来评估研究成果的准确性、原创性与质量是否达到相关学术期刊的发表标准。

在这套机制下，数学家会先将自己做出的研究成果撰写成数学论文，投稿到某个数学期刊，该期刊的编辑会根据论文的内容，将其交给相关领域的数学家匿名审阅，并根据审稿意见，决定是否刊发该篇论文，或者要求作者根据评审意见，对论文做相应的修改和说明。

物理、化学、生物等实验学科的同行评议，往往更侧重于实验设计的合理性和结论的启发性，不同于此的是，数学的学科特点要求进行同行评议的审稿人推导验证论文中的每一个定理和引理，确保逻辑零瑕疵。这也就导致了数学论文的审稿过程通常长达数月，甚至数年。对于那些宣称自己做出重大成果，解决重大猜想的数学家，其审稿过程往往会更加漫长和艰难。

例如，1993年安德鲁·怀尔斯（Andrew Wiles）将证明费马大定理的论文提交给“数学四大顶刊”之一的《数学年刊》（Annals of Mathematics）。编辑部指派了由尼古拉斯·卡茨（Nick Katz）领衔的6人专家组进行同行评议。最终，在修正了卡茨指出的漏洞之后，怀尔斯的工作以《模椭圆曲线和费马大定理》（Modular elliptic curves and Fermat's Last Theorem）和《某些赫克代数的环论性质》（Ring-theoretic properties of certain Hecke algebras）两篇论文的形式，发表在了《数学年刊》1995年第三期上。而这两篇论文，也是那一期《数学年刊》仅有的两篇论文。

数学界对格里戈里·佩雷尔曼（Grigori Perelman）证明庞加莱猜想的论文的验证工作则更加曲折。佩雷尔曼于2002年11月至2003年7月，将自己证明庞加莱猜想的论文公开发布在预印本网站（arXiv）上。由于其证明极其深奥，并且存在大量细节省略和步骤跳跃的情况，为了读懂佩雷尔曼的工作，在世界范围内，包括布鲁斯·克莱因（Bruce Kleiner）和约翰·洛特（John Lott）团队、约翰·摩根（John Morgan）和田刚团队、曹怀东和朱熹平团队在内的数学家，都对佩雷尔曼的工作进行了全面梳理，填补了细节，并发表了各种解读。

人工智能系统的出现，将有可能在未来改变数学界长久以来的同行评议机制。以高斯为例，这是专门用于自动完成数学证明形式化验证的AI系统，由两部分功能组合而成：自然语言推理（Informal Reasoning）部分，能够理解数学家用自然语言书写的数学论文；随后的形式化推理（Formal Reasoning）部分，则将其理解的论文转化为定理证明器Lean的程序代码并进行机器验证。

正如Math,Inc.公司首席执行官兼联合创始人杰西·韩（Jesse Han）在谈及高斯时所解释的：“高斯是一种特殊的推理智能体语言模型，能将传统的自然语言推理与完全形式化的推理相结合。因此，它能完成文献检索、调用工具、用计算机编写Lean代码、做笔记、启动验证工具、运行Lean编译器等一系列操作。”

面对维亚佐夫斯卡菲尔兹奖级别的工作，高斯仅用五天时间就完成了8维最佳球堆积问题证明的形式化验证，还发现并修正了已发表论文中的一处笔误。随后，24维最佳球堆积问题证明的形式化验证，也只花了两周时间就得以完成。

虽然高斯能极其高效地完成数学证明的形式化验证工作，但正如研发公司所介绍的，现阶段高斯的定位依然是协助顶尖数学家的自动形式化智能体。高斯的工作，仍然依赖于数学家将整篇数学论文拆解成前后相互关联的“小部分”，然后由高斯对其中每一部分进行逐一验证。

而这也正是菲尔兹奖得主、华裔数学家陶哲轩眼中未来的数学研究形态，数学家只需要负责提出想法和规划路线，往更深的数学前沿不断迈进，所有计算之类的“苦工”，都可以交给高斯这样的AI来完成。

如果说高斯的出现，可以大大减轻数学家的工作负担，并且加快数学结果的验证效率的话，那么董彬团队的工作则说明，对于数学研究工作来说，AI不仅仅是“苦力”这么简单。

和高斯一样，董彬团队研发的自动化AI框架也是由自然语言推理组件Rethlas和形式化验证组件Archon两部分组成的。但与高斯不同的是，董彬团队还构建了数学搜索引擎Matlas，其中包含了上千万条数学命题的陈述。通过Rethlas和Matlas的结合，董彬团队可以让他们搭建的AI以自然语言搜索已知的数学结果，并从中探索解决问题的想法和工具。而这也正是数学家们最常使用的工作方法。

最终，Matlas检索到了戴维·詹森（David Jensen）在2006年发表的一篇论文。这篇论文与这次AI所解决的安德森猜想并不相关，但是Rethlas发现，其中一个技术性的结果可以用来构造安德森猜想的一个反例，进而证明了安德森猜想不成立。

随后，Archon将这一结果转化成了约19000行Lean4代码，给出了这个结果的形式化机器验证。就这样，董彬团队研发的AI完全独立地解决了安德森猜想。这代表着AI可以在不依赖人类数学家给出指引的情况下，独立完成研究级别的数学工作。

如果说董彬团队的AI，还是专门为了解决数学问题而研发的，那么，高尔斯的个人使用经验，以及他对OpenAI官方新闻的震惊则表明，不仅仅是专业型AI，就连通用型的AI，都具备了进行数学研究、解决数学问题的能力。

这似乎意味着，迅猛发展的AI，开始逐渐进入数学这个原本只属于人类高级智力活动的领域。

AI在数学领域的这些进展，让人不由得去想，如果在不远的未来，AI能够更高效、更准确地解答数学问题，那么数学家这一职业还有存在的必要吗？

左图为艾伦·图灵（1912—1954），右图为约翰·冯·诺伊曼（1903—1957）。他们关于计算机和人工智能的奠基性工作，在当时都是作为纯粹的数学研究来进行的。（视觉中国/图）

表面上看，数学这门人类最古老的学科，似乎自诞生之初就没有变化，现在的数学家们仍然像两千多年前的阿基米德一样，主要靠纸笔演算的方式来进行研究。但是，实际上，数学家们对于新兴技术的出现，一直持开放态度。

“计算机科学和人工智能之父”艾伦·图灵（Alan Turing），以及提出了冯·诺伊曼架构的约翰·冯·诺伊曼（John von Neumann），在当时的身份都是数学家。他们关于计算机和人工智能的奠基性工作，在当时也都是作为纯粹的数学研究来进行的。当下AI热潮的底层原理和框架，同样来自数学家们在上世纪七八十年代的研究成果。

而当电子计算机出现之后，就有不少数学家在第一时间开始探索用机器证明数学命题的可能性。

1954年，在普林斯顿高等研究院重达2.3吨的真空管计算机JOHNNIAC上，美国数学家马丁·戴维斯（Martin Davis）用其编写的包含自然数和加法的算法程序，让JOHNNIAC证明了“两个偶数的和还是偶数”。

1956年，同样是在JOHNNIAC上，艾伦·纽维尔（Allen Newell）、赫伯特·西蒙（Herbert A. Simon）和J.C.肖（J.C.Shaw），用他们开发的程序“逻辑证明机”，证明了伯特兰·罗素（Bertrand Russell）的《数学原理》（Principia Mathematica）中前52条定理中的38条。对于某些定理，“逻辑证明机”甚至找到了新的、更优雅的证明。

1976年，数学家凯尼斯·阿佩尔（Kenneth Appel）和沃夫冈·哈肯（Wolfgang Haken），在美国伊利诺伊大学的IBM360电脑上，花费1200小时，验证了四色定理的所有1936种构型，从而证明了四色定理。自那之后，包括双泡猜想、罗宾斯猜想在内的数十个数学问题，以与四色定理类似的方式得到了解决或者取得了重要的进展。

但是，时至今日，仍有数学家在尝试不使用计算机，纯靠人力去证明包括四色定理在内的，那些已经通过机器证明得到解决的数学问题。其中的根本原因，就在于数学这门学科本身的价值观。

在普遍的认知中，数学家们的日常工作，就是证明各种数学定理、解决各种数学猜想，但是证明定理并不是数学家工作的全部。

伯恩哈德·黎曼（Bernhard Riemann）的很多工作用到了数学理论，例如黎曼映照定理的证明中用到的椭圆方程的正则性，直到20世纪很晚的时候才逐步建立起来。

对现代几何学的多个领域做出了革命性贡献的俄裔法国数学家米哈伊尔·格罗莫夫（Mikhaïl Gromov），他的很多论文，按照一般数学工作者的标准来看，已经远远超出了“不严格”的程度。为了理解格罗莫夫的一篇短短十来页的文章中的内容，往往需要很多数学家去写一系列的文章。

类似的情况还有物理学家出身，却拿下数学界最高奖菲尔兹奖的爱德华·威腾（Edward Witten）。他的很多工作，都来自物理学的直觉，而不是数学的严格。

很多数学上的想法，未必是严格的，但可能是很精彩的。无论是黎曼还是格罗莫夫和威腾，他们写下的“证明”都是充满内涵和启发性的。相较于一个严格的、没有错误的证明，这些“不严格”的工作能够让我们对数学的理解更加深入，从而发现更多未知的数学。就像陈省身所说的：“有数学经验和远见的人，能在大海航行下，达到重要的新的领域。”

其中所体现的，对未知的探索、对数学的远见和洞察力，以及提出新问题、新概念的能力，才是数学家最为珍贵的品质。这种品质，在数学家当中，被称为“数学品位”。

相较于证明猜想的数学家，那些提出猜想的数学家，在数学上也具有同样重要的地位。正因如此，诸如费马大定理、庞加莱猜想等等，都是以提出猜想的数学家的名字来命名的。

而对于已经获得证明的数学定理，数学家们也不会就此止步，而是会想方设法去探索新的证明方式，从中获取新的数学发展。例如，被很多数学家誉为二十世纪最伟大的两个定理之一的阿蒂亚-辛格指标定理（Atiyah–Singer index theorem）。自1963年迈克尔·阿蒂亚（Michael Atiyah）与艾沙道尔·辛格（Isadore Singer）证明该定理以来，数学家们在此后的几十年间，给出了数十种全新的证明。这些证明中所蕴含的思想和观点，极大地丰富了数学的内容。

因此，即使在未来，AI的发展使得其数学水平达到了远超人类数学家的程度，人类数学家也会去尝试理解AI所给出的数学证明，并从中吸收学习，做出自己的原创性工作。

正如德国数学家卡尔·雅可比（Carl Jacobi）在1830年写给法国数学家阿德里安-马里·勒让德（Adrien-Marie Legendre）的一封信中所说的：“科学的唯一目的是为了人类心智的荣耀。”

资料链接