为什么GPT-6 Astra让整个数学圈都炸裂了？

一、先认个名：Astra 是什么，为什么叫这个

Astra 是 OpenAI 在 2026 年 9 月 3 日发布的旗舰模型，GPT 系列的最新一档。名字源自拉丁语 astrum，意为"星辰、群星"——OpenAI 沿用了天体命名法：Astra 之上还有 Sol（太阳）、Terra（地球）、Luna（月亮），规则是"天体越大、能力越强"，所以排序是 Astra > Sol > Terra > Luna。发布前官方那句预告 "The stars are almost aligned（星星快对齐了）"，既是代号隐喻，也暗指算法、算力、工程与商业化的拼图即将合拢。

二、它到底做成了什么：分数很实，宣称很猛

先说站得住的。Astra 把连续素数间距上界从 246 推到 186（张益唐 2013 年从 7000 万起步，全球联手多年才到 246），且通过 Lean 形式化验证；在 Epoch AI 与曼彻斯特大学的 FrontierMath Erdős 基准里，它是唯一非零分的模型——68 道人类长期未解难题解出 2 道（放宽预算后 5 道），其余四个顶尖模型全交白卷。

更猛的是一则"宣称"。OpenAI 表示，一个比 Astra 更强的未发布内部模型，调度约 1 万个 AI Agent，在 88 小时内交换近 300 万条消息、产出约 1300 亿 token、耗费约千万美元，攻克了七大千禧年难题之一的 Navier–Stokes（纳维–斯托克斯）方程——证明"原本静止的光滑流体，可以在有限时间内出现奇点（有限时间爆破）"，随后由 GPT-6 Astra 再用 Lean 花 17 小时把证明形式化验证。

📐 一个比喻：把"影响"想成挖隧道过去一位数学家攻克难题，像一个人徒手挖一条隧道——卡在某层岩石上，可能耗去数年，还容易钻进死胡同钻不出来。Astra 带来的不是"多了一个更聪明的矿工"，而是：同一时刻，一万个不会疲倦、不会气馁、还共用一份永不丢失笔记的挖掘工，朝不同方向同时试；更关键的是，旁边坐着一个永远不睡觉的监理（Lean），每一步都重新验算、只认那个绿色对勾。隧道凿通的速度，自然不是一个量级——这，才是"影响有多大"最直观的注脚。

三、千禧年这道，到底算不算数

先科普：千禧年七大难题由克莱数学研究所于 2000 年设立，每题悬赏 100 万美元，至今只解出一道。Navier–Stokes 问的是：描述空气、水流动的方程组，其解是否永远光滑，还是会在某一刻"炸掉"。若 OpenAI 的宣称成立，这将是首道由 AI 攻克的千禧年难题——分量极重。

但三个保留必须写清楚，否则就是误导：

第一，它覆盖的是"受迫"版本（方程外加了外力项），而千禧年奖要求的是"无外力"版本；克莱研究所尚未认定这满足获奖条件。这差别不是咬文嚼字——无外力版本才对应流体在纯粹演化下会不会自发"炸掉"这一原问题，受迫版只是有意义的近亲。第二，整个证明未经独立验证，OpenAI 自己也说"不打算申领那 100 万美元"，把它定位成能力展示而非正式科学结论。第三，它卷进了一场数据与署名争议——纽约大学 Tristan Buckmaster 与 Anthropic 的 Levent Alpöge 此前用相近的爆破方法研究同一问题，部分草稿存于 OpenAI 的 Codex；Buckmaster 质疑对方是否借用了他们的思路，OpenAI 否认"调取过用户数据"，但承认"不能完全排除去标识化的使用数据间接改进了模型"。

真正值得记住的，或许不是"谁先谁后"，而是这套打法本身：把一道难题拆给上万个 agent 并行推进、互相借鉴思路，再用 Lean 把结果机检固化。这种"分而治之 + 形式化收口"的范式，比任何单一证明都更可能外溢到药物发现、材料科学和密码学验证。

所以，这一步是"声称"，不是"公认"。菲尔兹奖得主陶哲轩评价其底层思路是"了不起的成就"，但也未正式背书整个宣称。

四、Astra 是真 AI 吗，可靠吗

OpenAI 总裁 Greg Brockman 在发布会上说"欢迎进入 AGI 时代"。但独立评测机构 ARC Prize 提醒得很干脆：即便 Astra 在 ARC-AGI-3 上跑到 99.9%，也不等于 AGI 已经到来。耐人寻味的是，同一项测试 Astra 用标准配置只拿 62.7%，换上厂商适配框架才到 99.9%——说明成绩高度依赖"模型 + 工具 + 上下文"这整个系统，而不只是模型本身。

陶哲轩划的线最清楚：当前工具是"人工通用机灵（AGC），不是通用人工智能（AGI）"——靠随机、不可解释、需要强验证兜底的输出，偶尔还会犯蠢（比如一本正经地断言"所有奇数都是素数"）。它"有用却不够令人满意"，像一场被解释后就祛魅的魔术。

"如果过早地、用完全由 AI 驱动的方法把问题直接解决掉，尤其过程缺乏透明度，那这个问题原本能孕育数学进展的'过程'就可能被污染。严重时，AI 对整个数学发展的影响，甚至可能从正面变成净负面。"

—— 陶哲轩（菲尔兹奖得主，2026 ICM 公开演讲）

那它为什么在数学圈"显得可靠"？正因为数学的成果——证明——可以被 Lean 这样的机器内核自动核验。模型本身可以不可靠，但那个"绿勾"可靠。

📐 一个比喻：天才与公证员模型本身像一个可能说梦话的天才：它能写出惊世证明，也会一本正经地断言"所有奇数都是素数"。但数学给了它一个"公证员"——Lean 这样的机器内核，把证明逐行核验。天才可以胡说，公证员不会。Astra 之所以能进数学圈，不是因为它更"聪明"，而是因为数学恰好拥有物理、生物都不具备的特权：验证极廉价（verification is cheap）。它的可信，来自验证，而非来自智能本身。

📐 一个比喻：工作记忆的口袋DeepMind 的 Demis Hassabis 有个说法：上下文窗口相当于 AI 的"工作记忆"。人类工作记忆平均只能同时装下 7 个信息单元，AI 却被强行撑到了百万级——但"存得下"和"找得到"是两回事。这解释了为什么它能解 IMO 金牌题，却会在小学数学级问题上犯蠢：它的口袋很大，却不一定知道该从哪个兜里掏东西。

五、数学圈怎么评价：四股声音

封神派。宾夕法尼亚大学统计学家、OpenAI 研究员苏炜杰（北大数院 07 级）写道："我 9 岁第一次听说孪生素数猜想……这真是一个超现实的夜晚，亲眼看着我们的模型在我从小崇拜的问题上取得进展……就像见证了一个智能新时代的到来。"数学家 Bartosz Naskręcki 称 Astra 是"量子跃迁"，现在能边对话边在 Lean 里实时证明，"顿悟之后跟一个绿色对勾"，他说自己"不想回到只有顿悟的时代"。UC 伯克利的 Tony Feng、弗吉尼亚大学的 Ken Ono 也高度评价。

冷静派。Epoch AI / FME 基准把狂欢拉回地面：Astra 正式通过率仅 3%（2/68），扩展后 5 道，仍有 63 道未解，每解一题正式成本约 1 万美元；而千禧年那则"宣称"同样未经验证。结论克制："它证明的是 AI 正从'帮助解题'走向'参与发现'，而非已成为数学家的替代者。"

敲警钟派。除了陶哲轩的"AGC 不是 AGI"与"过程污染"警告，Buckmaster 的"算力截胡"质疑也指向同一红线：答案可以很炸，过程必须透明、署名必须干净。

落点。把四股声音摞一起，影响反而清晰：Astra 没让哪个数学家失业，却把"数学怎么做"的范式撬开一道缝——证明可以机器给、验证可以机器判、对话可以实时进行。

六、国内怎么看：清醒、务实、吃瓜三派

清醒派（学者）。北京大学朱松纯在 2026 世界人工智能大会上直言，"大模型即 AGI"是概念偷换——大语言模型本质仍是处理语言序列概率分布的统计模式匹配工具，不具备真正的理解、推理及因果认知能力；图灵奖得主杨立昆更激进，认为单纯的自回归生成式 AI 无法实现 AGI。上海财经大学特聘教授胡延平的态度最有代表性：Astra 局部个别小目标接近或达到了 AGI 水平，"但还不能说 AGI 已经完全到来"——按 OpenAI 自己的定义，"高度自主"这一条都还没实现。他主张用知识、泛化、任务、行动、感知、学习六个维度来"可视化"AGI 的进展。

务实派（评测与媒体）。国内多家机构没有被"AGI 降临"的热搜冲昏头。一篇流传很广的"中美欧三方测评"总结得很直白：英文硬核任务（数学、代码、网络攻防）Astra 确实是第一梯队，但中文语境下优势大幅缩水，"务实推进，但绝不迷信 AGI 口号"。财联社采访的国内 AI 资深人士也持审慎态度：Astra 已能在部分困难任务上达到甚至超过专家水平，但"尚未稳定覆盖大多数具有经济价值的工作"。

吃瓜派（开发者与网友）。这一派最热闹，也最真实。知乎答主"卜寒兮"算了一笔账：API 价格从前代每百万 token 4/20 美元涨到 10/50 美元，贵了 2.5 倍；有人实测让 Astra 搭建一座天坛祈年殿，直接花掉 200 美元 Pro 会员近一半额度，于是它得了个外号——"Token 榨汁机"。还有开发者吐槽它被强化出"防御性编程"的脾气：下个文件要校验 sha256，迁段代码要自己加一堆安全逻辑，"看了就绷不住"；发布当夜，评论区更是一片"等了半天不让用"的落差感。

一线华人数学家的特殊视角。风投机构 a16z 与两位身在风暴中心的年轻数学家的对谈值得拎出——Mark Sellke 与 Mehtaab Sawhney 都曾师从华人数学家赵宇飞，去年离开传统教职加入 OpenAI，直接参与这波研发。他们点破了范式转移的痛处："人类在一条死胡同里走得太远，最初的想法就会和失败细节纠缠，内在'上下文窗口'被污染，很难清空执念另辟蹊径；但 AI 不受情绪干扰，能冷静修正路径，甚至直接并行开启一个全新无污染的会话。"更反直觉的是审美："现在动辄写 200 页冗长证明的是人类，而 AI 驳倒近半个世纪未决的群论猜想，只用了区区 15 页。"当硬核推导的体力活被接管，他们判断人类的核心价值将转向"搭建框架、联通知识、把结论解释通透"——群体的认知整合，才是真正的护城河。

一个最妙的网络类比。有网友把 Astra 比作《三体》里"智子封锁解除后的技术爆炸"：过去几百年科学最稀缺的资源一直是高质量认知劳动，而 AI 第一次把它变成可大规模复制、并行运行的生产资料。Astra 自己的回应更冷静：数学很可能是第一个被彻底"工业化"的领域——未来不是一个数学家一年证 3 个定理，而是一个团队一天产生 10 万个候选定理，AI 自动证明其中 3000 个，人类研究其中 3 个，它管这叫 proof abundance（证明丰裕）。但紧接着补了一刀："Science becomes fast, engineering remains slow（科学变快，工程仍慢）——你一天能生成 100 万个抗肿瘤分子，却不可能一天完成 100 万个 I 期临床试验。"

所以看 Astra，别只盯着那串分数，也别被"AGI 时代"的口号带着走。真正该看的，是这群最不会被轻易忽悠的人怎么接招：有人看见星辰，有人盯着 62.7% 和那场署名战，有人死死按住"过程不能被污染"的红线，而国内的清醒派、务实派与吃瓜派，又各自在"是不是真 AI"上给出了不盲从的答案。数学圈对 GPT 的评价，本身就是这份影响最诚实的注脚——它没有改变"谁更聪明"，却正在改变"聪明这件事，还能不能只属于人"。