2026 年 8 月 1 日，OpenAI 官网挂出一篇没有演示视频、没有华丽配图的公告：内部版 Astra——他们的下一代主力模型——一次性解决了十道数学与理论计算机科学难题。这些题有的悬置了几十年，几代数学家啃过，其中几道连图灵奖得主都折过戟。公告发出一天内，Hacker News 上攒起 600 多条讨论。最让笔者意外的还是那个数字：OpenAI 说，这十道题的推理成本加起来，大约 2000 美元。
2000 美元是什么概念？一个数学博士的月薪都不止这个数。这意味着数学研究的试错成本，正在从「人年」变成「美元」。 需要说明的是，这个数字只是按公开 API 价格折算的推理费用，不包含训练模型的天价投入，也没有人知道 OpenAI 失败了多少次才成功。这两点，后面会细说。
图：OpenAI 官网为这十项进展发布的封面图。来源：openai.com
数学为什么这么难
先看看这些题的分量。十道题横跨高维几何、编码理论、群论、量子计算、密码学、图论。挑三道说：
「非 sofic 群是否存在」，群论领域的核心悬案，学界普遍相信存在，却二十多年没人构造得出来；「最近向量问题」的近似难度，密码学界盯了三四十年，它直接关系到量子计算机时代用什么加密；「多色拉姆齐数」的下界，出自传奇数学家埃尔德什（Paul Erdős）的问题清单第 183 号——这位数学家一生悬赏征解了上千道题。
为什么这些题这么难？数学证明就像在迷宫里找出口：每一步都必须有铁证，走错一步，前面全部作废。普通考试好歹有参考答案，数学难题没有——没人知道出口在哪里，甚至没人知道出口是否存在。人类数学家靠直觉、经验和运气，一次只能走一条路。
还有一层难处：这类题卡的是「第一个方向」。论证的起点错了，后面再精巧也是白费。几代数学家花几十年排除掉多少错误方向，没人统计过，但每个方向背后都是真实的人年。
AI 是怎么做到的
OpenAI 的做法可以概括成一句话：让模型自己生成成千上万个「草稿证明」，再用机器一一验明正身。
关键角色是 Lean。Lean 是一种形式化验证工具，相当于铁面无私的考官：把证明写成它认识的格式，它逐行检查逻辑，对就是对，错就是错，不看人情。AI 在训练时，能通过 Lean 检查的论证会得到奖励，于是模型学会了「写能被验证为正确的东西」。过去两年 AI 数学能力飙升，靠的就是这台自动阅卷机——数学是少数几个对错可以完全客观判定的学科：写作文不行，写代码凑合，数学可以。
可以想象成十万个分身同时钻进迷宫：大多数撞墙，少数走通，考官只认走通的那几条路。人类一次只能走一条路，AI 能同时试一万条，这是量级上的差异。
具体到这次：内部版 Astra 生成大量候选论证，Lean 筛选出站得住的；人类再把论证整理成论文，模型随后把每一步形式化，让机器可以复核；OpenAI 还公布了模型叙述自己思考过程的记录。十道题全部命中，合计约 2000 美元的 token。
为什么值得普通人知道
第一，AI 第一次交出了「人类没写过的新答案」。按 OpenAI 的说法，这些题的主结果至少十年没有实质进展。以前 AI 展示数学能力，多是解题、竞赛、复现已知定理，这次是真正悬置数十年的开放问题。
第二，数学是技术的上游。最近向量问题关乎后量子密码，球堆积和编码理论关乎通信与存储。数学地基每往前推一步，上面的技术迟早跟着动。
第三，成本曲线变了。数学家陶哲轩今年提出「大数学」：人类负责创意，AI 干粗活。2000 美元意味着，过去只有顶尖团队才做得起的海量试错，现在个人研究者也能碰。今年 5 月，OpenAI 用 AI 推翻埃尔德什单位距离猜想后，已有至少五篇人类论文沿着这个方向跟进——AI 的产出正在变成人类研究的起点。
对普通人来说，最直接的信号是：AI 能交出「人类没写过的新定理」，意味着它离「只会复述见过的东西」越来越远。这种能力不会只停在数学里，迟早流向工程技术——而技术最终会变成你我手机里的东西。
乐观派 vs 怀疑派：谁更有理
HN 讨论里，两派吵得不可开交。
| 立场 | 核心观点 |
|---|---|
| 乐观派 | 结果真实且可复核，Lean 形式化让造假空间极小；有人评价，若是一个学生解出其中几道题，大家会认为他未来有望拿菲尔兹奖；这正是 1997 年深蓝击败卡斯帕罗夫时刻的数学版 |
| 怀疑派 | 可能是「超大搜索空间 + 自动验证」的蛮力，不产生新思想；OpenAI 没公开提示词，也没公布失败次数；S 曲线 vs 指数曲线之争——进展也许更像爬山，未必像坐火箭；这类公告自带营销动机，宣称与证据之间隔着没公开的细节；1976 年计算机暴力验证四色定理曾让数学家不适，但也没改变学科 |
两派都有站得住的点。怀疑派最有分量的一击来自一位 HN 用户：Lean 只能证明「写对了的命题」，命题本身对不对，还得人类核对。机器验证的是推理过程，问题本身有没有被理解，机器不负责。乐观派的回应更简单：四色定理之后，它就是定理，五十年来谁也没能推翻。
落点
数学家群体的反应两极：有人写长文，称这是「数学的黑暗之夜」；有人觉得这是数学走向大众的起点。OpenAI 罕见地引用了数学界的《莱顿宣言》，承认争议存在，并选择公开证明、公开形式化代码、公开思考叙述——这份透明度在 AI 公司里不多见。
笔者无意预测 AI 会不会取代数学家。能确认的只有三件事：十道题确实解出来了，Lean 可复核；成本是 2000 美元量级；争论刚刚开始。笔者的立场是：把「证明是否成立」交给机器和同行评审，把「AI 是否理解数学」留给时间。至于 AI 算不算「真的懂数学」，更像哲学问题，时间会给出它的答案。
参考链接：
- OpenAI: Ten advances in mathematics
- HN 讨论 (item?id=49157930)
