“实验数学”新纪元：当计算机开始认证真理

OpenAI模型破解了埃尔德什的几何猜想，引发数学界对AI信任与归功的讨论。陶哲轩等学者积极推动计算机验证技术，开启大规模协作的实验数学时代。

数学界正在经历一场由人工智能驱动的震荡。在2026年5月20日，OpenAI发布了一项突破性成果：其研发的模型成功证伪了著名数学家Paul Erdős在80年前提出的一个关于“单位距离问题”的几何猜想。这个猜想原本认为，在平面上排列点以使尽可能多的点对具有相同距离的最佳方式是使用规则网格，但AI发现了一种更复杂的排列方式，使得点对数量的增长速度超过了预期。

Paul Erdős认为，要尽可能多地排列出彼此距离相等的点对，最好的方法是使用一个正则网格，并将点间距调整为尽可能多的点落在圆上。他推测，随着点的增加，点对的数量也会增加，但增幅仅为微小。而一个人工智能模型却发现了一种更复杂的排列点对的方法，使得点对的数量实际上以更快的速度增长。

人工智能生成了一个反例，用以反驳埃尔德什的网格排列理论，而这一反例并不容易直观理解。它涉及在高维空间中构建一个复杂的网格，然后将其投影到平面之上。但这幅图抓住了该思想的精髓。它展示了一种以类似方式构建的点排列。

这项发现被哈佛大学的Melanie Matchett Wood评价为“发现了一段美丽的数学”。OpenAI的研究员Sébastien Bubeck指出，该模型是一个通用的推理大语言模型，并没有使用任何数学专用的工具或软件，研究人员甚至没有对模型进行特定引导。有趣的是，数学界此前普遍相信该猜想是正确的，但模型却执意尝试证伪并最终成功。模型通过将高维空间中的复杂网格投影到平面上，找到了这一反例，并运用了代数和数论这两个古老领域作为工具。

然而，并非所有人都为此感到欢欣鼓舞。由于AI的证明过程更多依赖于对大量策略的耐心尝试而非人类式的创造性洞察，数学家们开始担心未来研究的验证与道德归属问题。截至2026年6月5日，已经有1590名专家签署声明，呼吁为AI在数学研究中的应用建立严格的护栏。曼彻斯特大学的Thomas Bloom指出，AI的推理过程有时并不可靠，尽管这次的证明相对容易验证，但互联网上已经出现了大量由AI生成的、连提交者自己都读不懂的长篇证明。

在这种不确定性中，菲尔兹奖得主陶哲轩(Terry Tao)成为了计算机辅助数学的倡导者。他在年仅10岁时就曾与Paul Erdős相识并受到后者的提拔。陶哲轩在2006年获得数学界的最高荣誉，但他并不满足于传统的独立研究模式。早在2014年，他就预言未来的数学研究将由数百人协作完成，并由计算机而非人类审稿人进行核查。

陶哲轩开始深度参与Lean这一形式化验证软件的学习与应用。他认为，虽然AI工具在数学前沿领域常常表现得像一个过度自信的本科生，但它非常适合处理那些可以被拆解为成千上万个微小子问题的复杂任务。他主导了名为“多项式弗赖曼-鲁扎猜想”的形式化项目，成功将一个重要的研究成果拆解为模块化的逻辑片段，吸引了包括斯德哥尔摩大学和伦敦几何与数论学院在内的众多年轻学者参与。

这种协作模式在2024年推出的“等式理论”项目中达到了顶峰。该项目旨在绘制4000多条代数定律之间的逻辑图谱，涉及的问题总量高达2200万个。陶哲轩惊叹于项目的推进速度，在短短48小时内就解决了绝大部分问题。尽管乌得勒支大学的Johan Commelin等学者担忧年轻人在这种项目中的贡献如何获得学术认可，但陶哲轩坚持认为，数学正在从一种纯粹的理论学科转向类似物理学的“实验科学”。

正如欧洲核子研究中心的大型强子对撞机通过大规模实验产生数据一样，陶哲轩的“实验数学机器”也在挖掘全新的数学构造。这种新模式不仅能验证真理，还意外地发现了许多传统视角下难以察觉的新领域。虽然这种变革也引发了诸如“浪费时间”的质疑，但陶哲轩已经展示了一种全新的可能：数学不再只是孤单天才的灵光一现，而是人类洞察力与机器验证力量的深度共盟。