在桌上洒一把绿豆，有多少对豆子恰好相距 1 厘米？
作者丨岑峰 陈嘉欣
编辑丨岑峰 林觉民
2026年5月19日，Google在山景城用了2小时发布16款产品，告诉世界：AGI的未来是一整套工具链。一天后，OpenAI在Twitter上发了一条推文，告诉世界：AGI的未来是一个能独立做数学证明的通用推理体。
推文的核心信息是：OpenAI的通用推理模型破解了数学家Paul Erdős在1946年提出的平面单位距离问题。这个问题在离散几何领域悬而未决了80年。
没有发布会，没有Keynote。只有发布后4个小时带来的1万+赞，和一句来自菲尔兹奖得主的评价。
菲尔兹奖得主Tim Gowers说："如果这是一篇人类投稿，被送到了《数学年鉴》编辑部，我被要求给出快速审稿意见，我会毫不犹豫地推荐接收。没有之前的AI生成证明接近过这个水平。"
同一天，Google展示了AI能做什么样的"工具"，OpenAI证明了AI已经能做什么样的"智力"。两者的差距，可能比16款产品到一条推文的距离还要大。
01
一个让数学家猜了80年的问题
在桌上洒一把绿豆，记录那些恰好相距 1 厘米的豆子对。有 n 颗豆子时，最多能找到几对？
这就是 Paul Erdős 在 1946 年提出的“平面单位距离问题”。80 年来，人类最聪明的头脑始终只能得到一个答案：约 2n 对。数学界长期认为，质的突破不可能存在。
作为 20 世纪最高产、最传奇的数学家，Erdős 留下的清单被视为数学界的“待办圣经”。而这次，OpenAI 的模型推翻了圣经。它发现了一类全新的点阵排列，使增长速度突破了线性限制，跃升至“超线性增长”。
打一个不太严谨但直观的比方：线性增长是沿着地面的平路走，超线性增长是开始上坡。平路走得再快也到不了山顶，但上坡可以。
外行人可能会想："模型用算力暴力搜索，找到了人类找不到的解。"
但实际情况完全不同。模型靠的不是算力，是代数数论，一个与几何完全不沾边的数学分支。它从数论的工具箱里借了一把钥匙，打开了那扇几何学家80年没打开的门。
为了确保这不是 AI 的“幻觉”，数学家们不仅逐行检查了AI的证明，还专门写了一篇配套论文来阐释它的思路。整个证明通过Lean软件做了形式化验证。这意味着它可以被计算机逐行追溯检查，不需要"相信"，只需要"验证"。
为什么形式化验证如此重要？数学史上发生过多起"著名证明后来被发现存在漏洞"的事件。1993年怀尔斯证明费马大定理时，第一版就被发现了一个关键漏洞，又花了一年多才修复。AI生成的内容如果不经过验证，同样可能"看上去很美，但某个细节错了"。Lean验证相当于给数学成果上了一道透明的保险：每一个推理步骤都可以被追查，不会因为谁的名气大就放水。
Erdős问题清单的管理人Thomas Bloom曾是AI证明的最尖锐批评者。七个月前，GPT-5.2当时声称解决了多个Erdős问题，后来被指出只是找到了文献中的已有解法。但这一次，他的态度转向了支持。让最硬的批评者点头，这比任何新闻稿都硬。
02
AI是怎么做到的：从"猜答案"到"推答案"
比"证出了什么"更值得追问的是"怎么证出的"。
技术写作者Adam Holter指出，模型的成功率随思考时间增加而提高。工作机制与传统AI完全不同。
传统AI模型推理是一次性的：输入问题，输出答案，没有修正。OpenAI的新模型会生成多条推理路径，自我评估，走不通就回溯。这与人类数学家的"试错"类似，区别在于AI能在毫秒级完成上百次试错。
这次突破验证了"推理时Scaling"（即"让模型想得更久"）。过去两年，业界发现：训练阶段变大是一条路，推理阶段"想"得更久是另一条路。思考时间从秒级延长到小时级，解决的问题从"高中奥数"跃升到"80年未解的数学猜想"。
这个验证同时反驳了"让模型多想只会把错误打磨得更光滑"的质疑。125页的推理链条中存在多个关键决策点，每个都需从备选方案中选择正确路径。若只是"打磨错误"，它不可能精准找到那条80年未被发现的路径。
据Holter描述，模型生成了长约125页的推理链。这不是"抄文献"，而是一连串决策：尝试一种工具，另一种理论提供可能，回头验证构造是否正确。模型在代数数论和离散几何之间跳跃，每一步都在论证、验证、修正。
这条125页推理链的价值在于：它不是猜的，是推出来的。
论文链接：https://cdn.openai.com/pdf/74c24085-19b0-4534-9c90-465b8e29ad73/unit-distance-proof.pdf
成果背后是一个分工框架。Holter认为，AI负责提出方案并验证，人类负责选择重要问题、判断结果重要性、塑造研究方向。AI做"发散"，大规模生成和探索构想；人类做"收敛"，判断哪些构想值得深挖。人的专业判断因AI提供更多选择而更加宝贵。
Tim Gowers的评论也印证了这一点。他说的是"如果这是人类论文，我会推荐接收"，而不是"数学家可以退休了"。
AI产出已达人类顶级期刊发表水平，但这个判断仍需人来做。
这一成果引发了讨论。Hacker News上的开发者已越过"AI能不能做数学"，转向"下一个是什么"。有人判断材料科学可能是下一个目标，因为材料设计是在超大空间中搜索最优结构，与数学证明逻辑相似。也有人预测药物分子设计会率先受益，因为模型"从抽象理论到具体构造"的推理链，正是从靶点结构推导候选分子所需的能力。
03
AI4S的两条路：
一个建实验室，一个培养研究员
AI4S赛道在2026年5月出现了两条截然不同的技术路线。
Google在I/O发布了Gemini for Science，面向科学家的AI工具包，包含三个实验性产品：Co-Scientist（自动生成假设）、AlphaEvolve加ERA（计算发现）、NotebookLM（文献洞察）。其逻辑是打造科研加速器：看论文、整理数据、生成假设。
OpenAI走了完全不同的路。它的通用推理模型独自完成了从产生想法、构造证明到验证结论的完整流程，超越了"辅助工具"定位，亲自完成论证。
两条路线的差异可以用三个问题来概括。
▪谁来定义问题？Google的工具需要科学家输入问题，系统生成假设并附引用，最终判断仍由人做。OpenAI的模型自己圈定方向，调动跨学科工具，走完全程。
▪适合什么场景？Google路径适合已有明确方法论的领域：跑标准流程、处理海量数据。OpenAI路径适合需要"跨学科借工具"的理论突破。
▪验证门槛多高？Google的成果经过同行评审，这是学术标准。OpenAI的成果经过外部数学家独立复核加计算机逐行验证，后者更严格，因为机器不看人面子。
更深层区别在于对AI4S的理解。Google的方向是"系统化"：建完备的科研基础设施，让科学家在上面跑研究。OpenAI的方向是"代理化"：训练通用推理体，直接参与最核心的智力环节。Google在建造实验室，OpenAI在培养研究员。
OpenAI研究员在做计算
理解了这个区别，就能理解Sam Altman为何说"心情复杂"：他的模型开始做他自己做不到的事了。不是帮他查资料，是替他做了最难的部分。这种感受难以用骄傲或恐惧简单描述，说明OpenAI自己也在消化这个事件的长期含义。
04
范式的重写：当AI成为科研伴侣
回到Tim Gowers那句话。
它的表层含义很直接：AI产出的数学成果已达人类顶级期刊可接收水平。这是菲尔兹奖得主的认可，而非OpenAI新闻稿的表述。
但深层含义更值得推敲。Gowers说的是"如果这是人类投稿"。意味着AI产出值得被认真对待，但最终判断权仍在人类手中。
科技媒体IC.Work提出了一套务实的检验框架，将AI数学发现的验证分为三个步骤：
1、公开细节：完整证明必须透明，Lean 验证必须通过。（已完成）
2、独立复核：专家群体反复拆解，寻找隐藏漏洞。（进行中）
3、稳定复现：同一个模型能否在其他难题上复制这种“直觉”？（关键点）
这套框架的价值在于：既不过度吹捧，也不过度贬低。三道关过了一道，说明值得严肃对待。第三道还没开始，说明离"AI数学时代"还有距离。
第三道关，即模型能不能在另一道数学难题上复现同样的水平，才是决定"里程碑还是孤例"的关键。如果能复现，数学研究的范式将发生根本性转变。
数学家将会获得一个没有学科偏见、不会疲劳的同事。你可以请它去数论领域找工具来解决几何问题，极大地缩短研究的摸索期。
验证将比发现更昂贵。当 AI 能源源不断提出新构造时，人类科学家的角色将从“寻找证明”转向“审判价值”。
这个问题已经越过了"AI能不能做"的讨论阶段，进入了"人类准备好了没有"的实践阶段。
回到开头那个场景。Google在I/O现场发布了16款产品，试图用工程化的方式把AI嵌入科学研究的每个环节；OpenAI在Twitter上发了一条推文，证明了AI已经能在最深层的逻辑突破中扮演核心角色。
这两条路最终可能会在同一个地方交汇：当工具足够聪明、也足够好用时，科学家就多了一个真正意义上的智力伙伴——一个能提出新想法、验证新假设、打破学科壁垒的伙伴。
这不是工具的胜利，而是科学发现从“手动时代”向“全自动化协作”跃迁的起点。
未经「AI科技评论」授权，严禁以任何方式在网页、论坛、社区进行转载！
公众号转载请先在「AI科技评论」后台留言取得授权，转载时需标注来源并插入本公众号名片。
热门跟贴