主页
2026 年 8 月 1 日,OpenAI 用「10 个悬置十年以上的开放数学问题的解答」官宣了下一代模型家族 Astra。本文讲清这波 AI 数学发现浪潮:它是什么、靠什么技术、边界在哪、数学界怎么看,以及对 Agent 工程的启示。
On August 1, 2026, OpenAI announced its next model family, Astra, by publishing solutions to ten math problems that had been open for a decade or more. This document explains the current wave of AI mathematical discovery: what it is, the technology behind it, where its limits are, how mathematicians are reacting, and what it means for agent engineering.
发生了什么:过去 15 个月里,AI 从「做数学竞赛题」跨到了「解真正的研究级开放问题」。标志性事件:2026 年 5 月 OpenAI 给出 1946 年提出的「单位距离猜想」的反例;此后 Erdős 问题清单上的开放问题接连被 AI 参与解决;8 月 1 日 OpenAI 发布报告,其内部模型 Astra 一次性解决 10 个开放问题,并全部用 Lean(一种能让计算机逐行核验证明的「形式化证明助手」)做了机器可验证的形式化。
What happened: Over the past 15 months, AI crossed from "solving competition math" to "solving genuine research-level open problems." The landmark: in May 2026, OpenAI published a counterexample to the Unit Distance Conjecture, open since 1946. Since then, open problems from the Erdős catalog have been falling one after another with AI involvement. On August 1, OpenAI released a report showing its internal Astra model solved ten open problems in one sweep — each formalized in Lean, a proof assistant whose compiler mechanically verifies every logical step.
为什么这对 Agent 工程师也重要:数学是长时程推理的「极限测试场」——问题定义清晰、答案可机器验证、没有含糊空间。支撑这些成果的技术(测试时计算、多智能体证明搜索、外部验证器闭环)正是当下 Agent 工程的三条主线。
Why this matters for agent engineers too: mathematics is the ultimate stress test for long-horizon reasoning — problems are precisely defined, answers are machine-checkable, and there is no room for hand-waving. The techniques behind these results (test-time compute, multi-agent proof search, verifier-in-the-loop) are exactly the three main threads of today's agent engineering.
要理解 8 月这波新闻,得先看这条 15 个月的演进线。此前 AI 数学的「天花板」一直是竞赛题——题目再难,也是人类已知答案的题。真正的分水岭是解出无人知道答案的问题。
To understand August's news, follow this 15-month arc. The previous ceiling for AI math was competition problems — hard, but with answers humans already knew. The real watershed is solving problems nobody knew the answer to.
节奏有多快?据 The Decoder 汇总:自 2026 年 5 月单位距离猜想被推翻后「闸门打开」,几乎每天都有 AI 参与数学研究的新消息;仅仅一周后,人类研究者就借用该证明的核心技巧推翻了另一个重要猜想(arXiv:2605.28781)——AI 产出的不只是结论,还有可复用的证明技术。另据社区统计(经陶哲轩确认合法性),Erdős 问题清单自 2025 年圣诞以来已有 15 题从「开放」转为「已解决」,其中 11 题标注了 AI 参与,且都做了 Lean 形式化。
How fast is the pace? Per The Decoder, after the Unit Distance refutation in May 2026 "the floodgates opened," with AI-in-math news landing almost daily. Just one week later, human researchers adapted the proof's core technique to refute another major conjecture (arXiv:2605.28781) — the AI produced not just a result but a reusable proof technique. Per community tallies (legitimacy confirmed by Terence Tao), fifteen Erdős problems have moved from "open" to "solved" since Christmas 2025, eleven crediting AI involvement, all formalized in Lean.
2026 年 8 月 1 日,OpenAI 发布数学报告(ten-proofs-oai.pdf),首次官方确认「Astra」这一「下一代主力模型家族」的名字,并给出其内部版本解决的 10 个开放问题。关键事实如下:
On August 1, 2026, OpenAI released its math report (ten-proofs-oai.pdf), officially confirming "Astra" as the name of its "next major model family," together with ten open problems its internal version solved. The key facts:
覆盖领域横跨高维几何、编码理论、群论、量子复杂性、格密码、极值组合。分量最重的结果之一是确立 non-sofic 群的存在性,解决了群论中的一个重大开放问题。运营 erdosproblems.com 的曼彻斯特大学数学家 Thomas Bloom 在 X 上称其为「big news」,认为在「构造」类结果里,这比 5 月的单位距离反例更重大。
The results span high-dimensional geometry, coding theory, group theory, quantum complexity, lattice cryptography, and extremal combinatorics. Among the weightiest: establishing the existence of non-sofic groups, resolving a major open question in group theory. Thomas Bloom, the University of Manchester mathematician who runs erdosproblems.com, called the results "big news" on X — in terms of constructions, bigger than May's unit-distance counterexample.
流程上值得注意的细节:模型独立产出数学论证后,人类与同一个模型协作把论证整理成论文,并完成 Lean 形式化;OpenAI 同时发布了每道题的推理过程走读。OpenAI 明确表示:论证本身出自 Astra,公司对其正确性负责;并援引 Leiden 宣言主张——对完全由 AI 生成的证明宣称人类作者身份,是对双方贡献的失实描述。
A notable process detail: after the model produced the mathematical arguments on its own, humans worked with the same model to turn them into papers and complete the Lean formalizations; OpenAI also published reasoning walkthroughs for each solution. OpenAI stated the arguments themselves came from Astra, that the company takes responsibility for their accuracy — and, citing the Leiden Declaration, that claiming human authorship for an entirely AI-generated proof would misrepresent both sides' contributions.
研究者 Noam Brown 坦言:OpenAI 也尝试过其他重大问题并失败,「遗憾,还没有千禧年大奖问题(yet)」。七个千禧年问题(每个悬赏 100 万美元)自 2000 年以来只被人类解决过一个,AI 至今为零。但他补充:每题投入其实不大,「测试时计算还能推得更远」。
Researcher Noam Brown was candid: OpenAI also tried and failed on other major problems — "Sadly, no Millennium Prize Problems (yet)." Of the seven Millennium Problems ($1M each), only one has been solved by humans since 2000, and none by AI. But he added that spend per problem was modest: "It's possible to push test-time compute much further."
背景一并交代:据 The Information(7 月 31 日,三位知情人),Astra 定位为与 Sol、Terra、Luna 并列的新模型类别,主打多 Agent 长时程协作;Sam Altman 已于 7 月 29–30 日在华盛顿向官员演示;它将成为美国政府拟议的模型发布前审查框架下首个受审模型。以 GPT-6 还是 GPT-5.7 的形式发布、何时发布,均未决定。OpenAI 的长期目标线:2026 年 9 月达到「研究实习生」水平,2028 年 3 月实现全自主 AI 研究员。
For context: per The Information (July 31, citing three sources), Astra forms a new model class alongside Sol, Terra, and Luna, built around multi-agent, long-horizon collaboration; Sam Altman demoed it to officials in Washington on July 29–30; and it is expected to be the first model reviewed under the U.S. government's planned pre-release framework. Whether it ships as GPT-6 or GPT-5.7, and when, is undecided. OpenAI's long-term line: "research-intern-level" skills by September 2026, and a fully autonomous AI researcher by March 2028.
当前的 AI 数学系统大致分两条路线,分歧点在「证明在哪个世界里被找到」:
Today's AI math systems split into two routes; the fork is over which world the proof is found in:
| 维度 | 路线 A:自然语言先行 | 路线 B:形式化原生 | Dimension | Route A: NL-first | Route B: Formal-native |
|---|---|---|---|---|---|
| 代表系统 | Astra / GPT-5.x Pro 系;Gemini Deep Think(IMO 2025 金牌即自然语言作答) | AlphaProof(IMO 2024 银牌)及社区所称 AlphaProof Nexus | Representative systems | Astra / GPT-5.x Pro line; Gemini Deep Think (its IMO 2025 gold was in natural language) | AlphaProof (IMO 2024 silver) and the community-reported AlphaProof Nexus |
| 验证时机 | 事后形式化(证明找到后再翻译) | 全程在编译器监督下搜索 | When verified | Post-hoc formalization (translate after finding) | Search under compiler supervision throughout |
| 已公开战绩(截至调研日) | 单位距离反例、Astra 十证明、多个 Erdős 题 | 据社区资料:9/353 Erdős 题、44/492 OEIS 猜想(单来源,未获官方页面印证) | Public track record (as of research date) | Unit-distance counterexample, Astra's ten proofs, several Erdős problems | Per community write-ups: 9/353 Erdős problems, 44/492 OEIS conjectures (single-source, not confirmed on an official page) |
| 适合场景 | 需要「灵感一跃」的构造、反例、跨领域组合 | 可在现有数学库上逐步搭建的定理、批量猜想清扫 | Best suited for | Constructions, counterexamples, cross-field leaps needing "flashes of insight" | Theorems buildable step-by-step on existing libraries; sweeping conjecture backlogs |
抛开头条,普通研究者(以及想借鉴方法论的工程师)今天实际在怎么用?综合 Saha、陶哲轩与 CMU 团队的公开描述,常见的是三种由浅入深的用法:
Headlines aside, how are ordinary researchers (and engineers borrowing the methodology) actually using this today? From the public accounts of Saha, Tao, and the CMU team, three usage tiers recur:
这套数学工作流对通用 Agent 设计的三条可直接借鉴的启示:
Three directly transferable lessons for general agent design:
① 找一个「Lean 等价物」:凡是能给任务配上硬验证器(编译器、测试套件、schema 校验、对账单)的场景,Agent 的可靠性都会发生质变——验证器把「概率性输出」变成「可拒收的产品」。这正是 rubric 式评测(如 Claude 的 Outcomes)背后的思想。
① Find your "Lean equivalent": wherever a task admits a hard verifier (compiler, test suite, schema check, reconciliation), agent reliability changes in kind — the verifier turns probabilistic output into a rejectable deliverable. This is the idea behind rubric-based evaluation (e.g. Claude's Outcomes).
② 把预算当一等参数:十证明 ≈ $2,000 说明「再想久一点」是有明码标价的旋钮;Agent 系统应把测试时计算(重试、并行采样、思考时长)做成可配置项,而非隐藏常量。
② Treat budget as a first-class parameter: ten proofs ≈ $2,000 shows "think longer" is a knob with a price tag; agent systems should expose test-time compute (retries, parallel samples, thinking time) as configuration, not hidden constants.
③ 多 Agent 要算协调税:数学搜索天然可并行(不同证明思路互不干扰),所以多智能体收益大;强耦合任务则未必——先问你的任务像哪一种。
③ Price in the coordination tax: proof search parallelizes naturally (independent proof attempts don't interfere), so multi-agent pays off; tightly coupled tasks may not — ask which kind your task resembles first.
头条容易造成「数学已被攻克」的错觉。Epoch AI 的 FrontierMath 系列基准提供了更冷静的标尺——它专为抗饱和设计,题目由职业数学家出、绝大多数从未公开:
Headlines can create the illusion that math has been conquered. Epoch AI's FrontierMath benchmarks offer a cooler yardstick — deliberately designed to resist saturation, with problems written by professional mathematicians and mostly unpublished:
另一个边界是领域不均衡:数学家 Trefor Bazett 指出,图论等领域特别适合机器生成证明,另一些领域则明显「抗药」。每解决一题的背后,是更多题依然无从下手。还要记住汇率:AI 解的多是「陈述清晰、可暴力+巧思组合攻破」的问题;千禧年级问题需要的可能是全新数学框架,而不只是更多算力。
Another boundary is field imbalance: mathematician Trefor Bazett notes that fields like graph theory suit machine-generated proofs especially well, while others remain resistant. Behind every solved problem stand many more with no known angle of attack. Mind the exchange rate, too: AI's wins are mostly cleanly-stated problems crackable by brute force plus clever construction; Millennium-level problems may require entirely new mathematical frameworks, not just more compute.
数学界的反应谱系比任何头条都有信息量。按乐观到悲观排列:
The spectrum of mathematicians' reactions carries more information than any headline. From optimistic to dark:
「在我的研究领域,前沿模型至少相当于一个扎实且不知疲倦的博士生。……有人会很快适应,发现无限可能;也有人会像民谣英雄 John Henry 一样,怀疑到最后一刻。」
"At the moment, in my area of research mathematics, frontier AI models are at least as good as a solid and indefatigable PhD student. … Some will adapt soon, and find boundless possibilities; other academics will continue to be AI-sceptical until the very end, like the folklore hero John Henry."
陶哲轩在 ICM 2026 演讲中把当下类比为 20 世纪初的数学基础危机:那场危机最终让数学地基更牢。他提出「证明过载」问题——结果产出的速度将超过人类审读消化的速度,数学家的角色会转向:判断哪些结果重要、如何呈现、研究该追求什么目标。他 2023 年预言「AI 到 2026 年成为可靠合著者」,已然应验。
In his ICM 2026 talk, Terence Tao compares this moment to the foundational crisis of the early 20th century — a crisis that ultimately left mathematics on firmer ground. He warns of "proof overload": results arriving faster than humans can review and absorb, shifting mathematicians' role toward deciding which results matter, how to present them, and what goals research should pursue. His 2023 prediction that AI would become a reliable co-author by 2026 has come true.
「感觉非常奇怪、且并不愉快——脚下的地毯就这样被抽走了。」Gowers 说 GPT 5.6 Pro 两次一击解出他投入大量时间的问题。他最担心的是「数学文化的可能毁灭」:如果不再有人花多年建立深层专业素养,一二十年后文献可能膨胀到没有任何人类共同体真正理解它。
"It felt very strange and not particularly pleasant to have the rug pulled out from under my feet like that." Gowers says GPT 5.6 Pro twice solved, on the first attempt, problems he had worked on at length. His deepest worry is "the possible destruction of mathematical culture": if fewer people spend years building deep expertise, the literature could balloon within a decade or two with no human community that truly understands it.
「最近的 Leiden 宣言,在我听来是一声捂住的尖叫。」数学家 Kirwin Hampshire 在《数学的暗夜》中直指要害:创造新数学历来是人类触及「不可言说之物」的方式之一;当每个定理都可能已在「巴别图书馆」中被机器写完,为什么还要让作者忍受这场噩梦?
"The recent Leiden Declaration on Artificial Intelligence and Mathematics is, to me, a well-muffled scream." In "The Dark Night of Mathematics," Kirwin Hampshire cuts to the core: creating new mathematics has historically been one way humans access the ineffable; if every theorem may already sit finished in a machine's Library of Babel, why force authors to endure that nightmare?
制度层面的回应是 Leiden 宣言:3000+ 数学家签名、国际数学联盟支持,不反对 AI,但要求使用透明、保护作者权利、人类对结果负责。Gowers 未签但表示大体支持。同时值得记住 Bloom 对「AI 取代数学家」叙事的反驳:这些 AI 建立在一个多世纪的数学理论上、由数学家建造、拿数学家写下的一切训练——把它的成果说成「取代」数学家,逻辑不通。
The institutional response is the Leiden Declaration: 3,000+ signatures, backed by the International Mathematical Union — not anti-AI, but demanding transparency of use, protection of authors' rights, and human responsibility for results. Gowers hasn't signed but broadly supports it. Also worth keeping is Bloom's rebuttal of the "AI replaces mathematicians" narrative: these systems draw on over a century of mathematical theory, were built by mathematicians, and were trained on everything mathematicians ever wrote — calling that "replacement" doesn't parse.
图 4 的阶梯是最好的解毒剂:最高两档仍是 0。AI 强在「广度 + 不知疲倦 + 便宜」(十题 $2,000),不在「深度的新框架」。目前所有重大成果的论文化、审查、意义判断仍由人类完成。
The ladder in Fig. 4 is the best antidote: the top two tiers are still at zero. AI's strength is breadth + tirelessness + cheapness ($2,000 for ten problems), not deep new frameworks. Every major result still gets its write-up, review, and significance judgment from humans.
Lean 只保证逻辑正确,不保证数学上有趣。陶哲轩早先评论 GPT-5.2 解出 Erdős 题时就提醒:那更多说明「速度」而非「难度」。正确性验证已自动化,重要性判断没有——这正是 Tao 说数学家角色转移的方向。
Lean guarantees logical correctness, not mathematical interest. When GPT-5.2 cracked an Erdős problem, Tao cautioned the win said more about speed than difficulty. Correctness checking is automated; significance judgment is not — exactly where Tao says the mathematician's role is moving.
长时程系统的两大顽疾(误差复利、上下文膨胀)并没有被宣布解决;Google–MIT 研究还表明强耦合任务上多智能体可能负收益。数学是「验证器完美 + 天然可并行」的最优场景——你的业务任务未必满足这两条,迁移预期要打折。
The two chronic ills of long-horizon systems (compounding errors, context growth) have not been declared solved; the Google–MIT study shows multi-agent can go negative on tightly coupled tasks. Math is the best-case scenario — perfect verifier, naturally parallel. Your business task may satisfy neither; discount accordingly when transferring expectations.
Astra 本身没有发布:无日期、无定名(GPT-6 还是 5.7 未定),能力叙述部分来自 The Information 的匿名信源。本文中「AlphaProof Nexus」的具体战绩数字同样来自社区资料、未见官方页面印证,已在表格中标注。阅读这个领域,来源等级意识(官方论文 > 官方博客 > 大媒体 > 社区)是基本功。
Astra itself is not released: no date, no final name (GPT-6 vs 5.7 undecided), and parts of the capability story come from The Information's anonymous sources. Likewise, the specific "AlphaProof Nexus" tallies here come from community write-ups without an official page confirmation, as flagged in the table. In this field, source-tier awareness (official paper > official blog > major press > community) is table stakes.
按「先读什么」排序:
In suggested reading order:
AI 数学发现 = 长时程搜索(测试时计算 + 多智能体)× 硬验证器(Lean)。前者提供野蛮的探索广度,后者把探索产物点石成金为可信知识——而这对组合,正是所有严肃 Agent 系统的原型设计图。竞赛已经毕业,开放问题刚刚破门,最高峰纹丝不动:2026 年 8 月的真实坐标,就在这三句话之间。
AI mathematical discovery = long-horizon search (test-time compute + multi-agent) × hard verifiers (Lean). The former buys brute exploratory breadth; the latter transmutes its output into trusted knowledge — and that pairing is the prototype blueprint for every serious agent system. Competitions: graduated. Open problems: door just cracked. The summits: unmoved. The honest coordinates of August 2026 sit between those three sentences.