OpenAI发布722篇数学论文，验证压力转嫁学界

上周，关于“数学家是否可以忽略人工智能”的讨论仍在发酵。紧接着，OpenAI 发布了 722 篇数学论文作为回应。这一举动在数学界引发了持续的关注与处理压力。尽管这看似是前所未有的局面，但在数学史上其实存在类似的先例。

要理解这一事件的影响，首先需要明确两个核心问题：数学流对人工智能意味着什么？反之，对数学本身又意味着什么？目前的证据显示，领先的人工智能模型已能批量生成具有研究水平的数学成果。OpenAI 使用了一种未公开名称的内部模型，据称每个结果平均消耗相当于 3 小时 ChatGPT Pro 的思维计算时间。ChatGPT Pro 是该公司的最高级订阅服务，月费介于 100 至 500 美元之间。

数学的黄金时代即将到来，数学家们正在发疯。

需要注意的是，“平均”一词在此处掩盖了巨大的成本差异。由于 OpenAI 的订阅服务存在大量补贴，难以准确核算单次结果的真实成本，且公司未披露具体数据。然而，考虑到上个月公司在纳维尔-斯托克斯方程问题上取得的突破所需投入的巨大算力，此次数学论文生成的平均努力程度似乎不太可能与之相当。

OpenAI 此举并非旨在打造一台纯粹的“数学机器”。这种显性的数学能力是否预示着其他科学领域的类似进展？目前看来可能性不大。

数学对于人工智能成功的关键在于其“可验证性”。文学创作缺乏客观衡量标准，无法确认 AI 能否写出媲美莎士比亚的作品；但数学拥有明确的逻辑基准。通过将证明形式化，转化为 Lean 等计算机代码，可以为提升 AI 数学能力提供闭环反馈：生成证明、形式化验证、奖励模型准确性。在其他缺乏此类验证闭环的领域，AI 模型的进展往往更为艰难。

值得注意的是，OpenAI 最新发布的这批论文中，正式化工作尚未完成。虽然其 Lean 证明目录列出了 722 篇论文中的 162 篇主要结果已完成形式化，但若统计附有任何 Lean 代码的结果，数量则上升至 235 个。总体而言，大部分工作仍处于未完成状态。

验证的挑战

这对数学界意味着什么？对于已完成形式化的证明，数学家可以确信其准确性。但对于其余部分，OpenAI 将繁重的验证工作留给了人类数学家。加州大学洛杉矶分校的特伦斯·陶（Terence Tao）曾形象地将此比作“将生肉尸体倾倒在我们共同的村庄餐桌上”。

为何 OpenAI 没有完成全部形式化工作？原因可能包括发布压力的驱动，使其选择公布结果而非继续等待。尽管 OpenAI 声称遵循了独立数学和人工智能咨询小组（AGMAI）的指导方针，但 AGMAI 随后澄清，其咨询角色不应被解读为对该发布的支持。

当前局势下，数学界已被迫面对这一现实。无论谁按下按钮，OpenAI 使用的内部模型至少提供了比完全免费工具更大的控制权。但这并不意味着 OpenAI 可以置身事外，正如 AGMAI 所指出的，AI 公司有责任协助人类理解其结果。

另一个更深层的原因可能是技术限制：OpenAI 的部分结果可能超越了当前的形式化技术能力。大多数 Lean 形式化依赖于由社区手工构建的 mathlib 存储库，类似于一个乐高积木池。其他形式化工作需在此基础上建立。一些 OpenAI 的结果需要全新的基础构件，而这些构件目前不在池中。在某些情况下，创建这些新构件可能比撰写非正式证明更加困难。形式化结果在数学各子领域的分布不均，暗示了某些领域可能存在形式化机制的真正瓶颈。OpenAI 在新闻稿中表示，随着更多形式化工作的推进，公司将更新存储库。

OpenAI 宣布解决了 10 个长期存在的数学问题

伦敦帝国理工学院的 Kevin Buzzard 指出，全面的形式化不仅涉及论文本身，还包括所有参考文献。AI 或许能填补空白，关键在于需要填补多少。目前的主要障碍在于形式化所需的时间成本。

为了评估影响规模，可以进行历史对比。这数百篇未经外部检查的非正式数学论文，大致相当于 arXiv 预印服务器每天发布的数学论文总量，尽管这一比较并不完全公平。另一种参照系是《数学年鉴》（Annals of Mathematics）收录的论文数量，但并非 OpenAI 的每一篇论文都达到该期刊的标准。

洪水已经打开

回顾历史，数学家们如何处理不确定的数学成果，可为未来提供路线图。有三个典型案例值得参考。

首先是斯里尼瓦瑟·拉马努金（Srinivasa Ramanujan）。这位自学成才的数学家将其作品寄给当时的权威 G.H. Hardy。Hardy 起初忽视信件，直到意识到其中蕴含真正的数学洞察力。两人开始合作，但拉马努金因病于 32 岁去世。他的笔记本，包括 1976 年发现的“丢失笔记本”，至今仍被数学家研究。

其次是托马斯·黑尔斯（Thomas Hales）的案例，展示了形式化的价值。1998 年，当时在密歇根大学的黑尔斯发表了开普勒猜想的证明方法。由于证明极其复杂，《数学年鉴》的审稿人花了四年时间评估，最终仅表示有 99% 的把握认为证明正确。黑尔斯随后花费十多年时间进行形式化证明，这是一项巨大工程，因为当时现代形式化工具尚不存在。

最后是望月新一（Shinichi Mochizuki）的情况。2012 年，这位日本京都大学数学家发表了关于 ABC 猜想的密集论文，被同行称为“外星数学”，其真实性至今仍有争议。目前正在进行形式化工作，但进展甚微。

当前数学家面临的处境，类似于同时面对数百名拉马努金、黑尔斯或望月新一。关键问题是：OpenAI 及其模型更接近哪一类？拉马努金英年早逝，无法协助他人理解；望月新一常被视为不愿解释其理论。希望 OpenAI 能成为黑尔斯式的模范，领导致力于形式化和促进理解的努力。这是 AGMAI 的要求，球在 OpenAI 脚下。目前尚不清楚这一目标是否会实现：本周《连线》杂志报道称，一名匿名 OpenAI 员工认为人工智能已经使数学“死亡”。

为什么 OpenAI 的千年奖数学突破引发争议？

更多人工智能阅读：

• OpenAI 首席执行官 Sam Altman 在接受 Politico 采访时表示：“世界应该接受一些坏事发生。”他认为这并非不合理的立场，互联网和智能手机等技术发展中也存在类似情况。
• 一位软件开发人员利用人工智能解决了与 Venn 图相关的问题，这成为业余数学家借助新工具取得进展的又一例证。
• 保险公司正在考虑 AI 代理入侵其他公司时的责任归属。由于涉及意图认定问题，法律上对于此类事件中受影响方的界定仍存在不确定性。
• 佛罗里达州一名妇女因在与 Claude 的聊天中对警长办公室发出威胁而被捕。Anthropic 的自动化系统将威胁标记为担忧事项，经人类审查员确认后触发报警。
• 教皇莱昂十四世就人工智能艺术发表看法，持批评态度。他指出，艺术与基于数百万图像统计计算生成的内容之间存在本体论上的差异，甚至大于美学差异。他写道：“算法缺乏人类的火花。”值得注意的是，他并非首位参与 AI 艺术辩论的教皇。