2000美元。
这不是一台高端游戏本的价格，这是OpenAI解决10道困扰数学家数年到数十年的开放问题所花的全部算力成本。8月1日，OpenAI发布了一份题为《Ten advances in mathematics and theoretical computer science》的研究报告，第一次公开了其下一代模型家族Astra的存在——不是通过跑分榜单，不是通过聊天demo，而是直接甩出来10个数学和理论计算机科学的开放问题，附带完整的Lean形式化证明，任何人都可以在GitHub上独立验证。菲尔兹奖得主Timothy Gowers看完其中一项证明后说："毫不犹豫可以推荐给《数学年刊》。"
249页论文，62页解题思路，10个横跨群论、高维几何、编码理论、量子复杂度、格密码学和极值组合学的证明，全部由Astra多智能体系统自主完成，Lean形式化转换耗时约一周。这不是AI帮数学家算算数、打打下手——这是AI第一次在前沿数学领域做出了人类做不出来的原创成果。
为什么是数学？为什么是Lean？
OpenAI选择数学作为Astra的首次公开亮相，是一个极其精明的策略。
过去两年，大模型的能力展示几乎被跑分榜单垄断。MMLU、HumanEval、MATH、GPQA——每个新模型发布，都会甩出一长串benchmark数字，然后社区开始争论有没有数据污染、有没有刷榜、测试集是不是被见过了。跑分可以被质疑，可以被操纵，可以通过prompt工程刷高分数。但数学证明不一样。
一个数学证明要么对，要么错。尤其是形式化证明——用Lean这种证明助手语言写出来的证明，计算机可以逐行验证逻辑正确性，不存在"大概对""基本正确""评委觉得好"的模糊空间。你构造了一个非sofic群，推翻了Gromov 1999年提出的"所有可数群都是sofic的"猜想，这个证明要么成立要么不成立，任何数学家都可以下载代码跑一遍验证。
这也是为什么OpenAI这次没有发布产品、没有公布参数规模、没有开放API——他们用一种无法造假的方式展示了Astra的能力。当一个AI可以独立做出可机器验证的原创数学证明时，你再去质疑它的推理能力就显得苍白了。
10个问题中最引人注目的两个：一是构造出无限有限呈现的非sofic群，终结了数学家Gromov在1999年提出的猜想——这个问题等了27年；二是找到了Erdős单位距离猜想的反例，这个关于平面上单位距离点对最大数量的经典问题被Astra找到了反例。其他问题覆盖了高维球体堆积、算术电路复杂度下界、算子代数、量子计算复杂度等前沿方向。Epoch AI的OpenMath评分体系将非sofic群构造评为"突破"级别，认为有望成为全年数学领域最佳成果之一。
2000美元的真正含义
如果说证明本身是能力的展示，那2000美元这个数字才是真正的产业炸弹。
密歇根大学数学研究者马骁在接受采访时做了一个对比：传统上，一项工业级协议的形式化证明可能需要5个数学PhD花2年时间，成本数百万美元。而Astra把这个成本压到了原来的1%。这不是效率提升30%或者50%，这是成本结构的彻底重构。
想想这意味着什么。数学研究的瓶颈从来不是"有没有足够多的聪明人"——全世界顶级数学家的数量是极其有限的，一个菲尔兹奖级别的成果可能需要一个天才花十年时间。但如果AI可以把证明的成本从"稀缺天才的十年光阴"变成"2000美元的算力"，那数学研究的产能瓶颈就从人脑转向了算力。这不是取代数学家，而是给每个数学家配了一支不知疲倦的研究生军队。
"过去形式化验证太贵没人用——一项工业级协议的证明可能要5个PhD干2年。现在可以用Astra类模型把成本压到1%。这是数学的'前Claude Code时代'的终结。"—— 密歇根大学数学研究者马骁
更直接的影响在软件工程领域。形式化验证（formal verification）一直是保证软件正确性的黄金标准——用数学方法证明代码没有bug——但因为成本太高，除了航空航天、加密协议、芯片设计等极少数领域，几乎没人用得起。如果AI可以把形式化证明的成本降到几千美元，那未来关键软件系统——操作系统内核、加密库、智能合约、AI自身的安全约束——都有可能被数学化地证明正确。
这不是科幻。Astra证明的10个问题中，有几个本身就是关于算术电路复杂度和格密码学的——这些正是计算机科学和密码学的基础问题。当AI可以证明数学定理，它也可以证明代码的正确性，证明加密方案的安全性，甚至证明AI系统自身的行为符合预期。
Astra是什么：多智能体系统，不是聊天机器人
从公开信息看，Astra不是一个单一的大模型，而是一个多智能体协作系统。
它的工作方式更像一个数学研究团队：有智能体负责理解问题和检索文献，有智能体负责提出证明思路，有智能体负责把思路翻译成Lean代码，有智能体负责检查证明漏洞，有智能体负责修复错误。多个智能体在一个协作框架中反复迭代，直到产出一个完整的、可机器验证的证明。这个过程和人类数学家做研究的方式极其相似——提出猜想、尝试证明、发现漏洞、修正方向、最终定稿。
值得注意的是，OpenAI选择在这个时间点公开Astra，和Sam Altman近期在华盛顿的活动有微妙的呼应。就在Astra发布的同一周，Altman带着GPT-6（内部代号）赴白宫向议员预览，美国政府正在酝酿前沿AI监管框架。用AI攻克数学难题这种"为国争光"式的成果，在政策对话中显然比"我们又做了一个更强的聊天机器人"更有说服力。
当然，Astra的能力边界也需要冷静看待。这10个问题集中在数学中规则明确、答案可形式化验证的领域，这恰好是当前AI最擅长的——符号推理、逻辑演绎、在严格定义的空间内搜索。而在需要直觉跳跃、跨领域联想、物理世界建模的数学研究中（比如几何拓扑、数学物理），AI能否同样有效，目前还是未知数。你不能指望一个连杯子都抓不稳的机器人明天就证明黎曼猜想。
从辅助工具到原创者的临界点
把时间线拉长，你会发现Astra代表了一个真正的分水岭。
过去所有AI能力展示——写代码、做翻译、画画、写文章、甚至发现新的抗生素——本质上都是在执行人类已经定义好的任务。AI做得更快更便宜，但任务的边界是人类划定的，评价标准是人类制定的，产出是人类已知范畴内的东西。2023年的GPT-4可以通过律师资格考试，但它不会提出新的法学理论；2024年的Claude可以写代码，但它不会发明新的算法范式。
Astra不一样。它解决的是人类没有解决的问题，而且证明是可以独立验证的。这是AI从"执行已知任务"到"探索未知领域"的关键一步。
未来的影响可能在三个层面展开：
第一，数学和理论计算机科学的研究加速。如果证明成本足够低，数学家可以把精力集中在提出好问题和建立大框架上，把繁琐的证明细节交给AI。这就像计算器没有让数学家失业，反而让他们能研究更复杂的问题一样。
第二，形式化验证从奢侈品变成日用品。当证明一个系统正确性的成本从几百万美元降到几千美元，关键基础设施软件、金融系统、AI安全约束都可以被数学化验证。这可能是AI安全领域最重要的技术路径之一——不是让AI"有道德"，而是用数学证明它的行为边界。
第三，AI辅助的AI研究加速。如果AI可以证明数学定理，它也可以证明新算法的正确性、优化模型架构的数学性质、甚至设计更高效的神经网络结构。这是一个递归的自我改进循环——AI帮助改进AI，速度会越来越快。
当然，这里有一个哲学问题：如果一个AI证明了一个定理，但没有人类能理解证明的全部细节（因为太长太复杂），这个证明算谁的？Astra的某些证明可能已经接近这个边界——人类可以验证每一行Lean代码是对的，但整体证明的"思想"可能超出了单个人脑的把握能力。这在数学史上不是新鲜事——四色定理的计算机证明在1976年就引发过类似争论——但AI把这个问题推到了前所未有的规模。
2000美元。下次你打开ChatGPT或者Claude聊天的时候，想想这个数字。你输入的每一个token背后，不只是服务器在消耗电力——还有一个正在快速成长的"AI数学家"，它用一台笔记本电脑的价格，做出了人类几十年没做出来的数学发现。数学是科学的皇后，形式化验证是工程的基石。当这两件事同时被AI以极低成本攻克，整个科研和工程的范式都会被重写。
明天见。
$2,000.
That's not the price of a high-end gaming laptop. That's the total compute cost for OpenAI to solve 10 open problems that stumped mathematicians for years to decades. On August 1, OpenAI published a research report titled Ten Advances in Mathematics and Theoretical Computer Science, publicly revealing its next-generation model family Astra for the first time — not through benchmark leaderboards, not through chat demos, but by dropping 10 unsolved problems in math and theoretical CS, complete with formal proofs in the Lean proof assistant that anyone can independently verify on GitHub. Fields Medalist Timothy Gowers, after reviewing one proof, said he would "unhesitatingly recommend it to the Annals of Mathematics."
249 pages, 62 pages of proof sketches, 10 proofs spanning group theory, high-dimensional geometry, coding theory, quantum complexity, lattice cryptography, and extremal combinatorics — all produced autonomously by Astra's multi-agent system, with Lean formalization taking roughly one week. This isn't AI helping mathematicians crunch numbers or do grunt work. This is the first time AI has produced original frontier-mathematics results that humans couldn't.
Why Math? Why Lean?
OpenAI's choice of mathematics for Astra's debut is a brilliantly calculated move.
For the past two years, LLM capability demonstrations have been dominated by benchmark leaderboards. MMLU, HumanEval, MATH, GPQA — every new model drops a battery of scores, and the community argues about data contamination, benchmark gaming, and whether test sets were seen in training. Benchmarks can be questioned, gamed, inflated through prompt engineering. Mathematical proofs are different.
A mathematical proof is either right or wrong. Formal proofs in particular — written in proof assistants like Lean — can be verified line-by-line by computer for logical correctness. There is no "roughly right," no "mostly correct," no "the reviewers liked it." You construct a non-sofic group disproving Gromov's 1999 conjecture that all countable groups are sofic, and either the proof holds or it doesn't. Any mathematician can download the code and run it.
This is why OpenAI didn't release a product, didn't announce parameter counts, didn't open API access — they demonstrated Astra's capability in a way that cannot be faked. When an AI can autonomously produce machine-verifiable original mathematical proofs, questioning its reasoning ability becomes a hollow exercise.
Two results stand out among the ten. First, the construction of a finitely presented infinite non-sofic group, resolving a conjecture posed by Gromov in 1999 — a problem that waited 27 years. Second, a counterexample to the Erdős unit distance conjecture, a classical problem about the maximum number of unit-distance pairs in a plane. Other problems cover high-dimensional sphere packing, arithmetic circuit complexity lower bounds, operator algebras, quantum computational complexity, and more. Epoch AI's OpenMath rating system classified the non-sofic group construction as "breakthrough" level, with potential to be among the year's best mathematical results.
What $2,000 Really Means
If the proofs themselves demonstrate capability, the $2,000 figure is the real industry bombshell.
University of Michigan mathematics researcher Ma Xiao drew a comparison in an interview: formally verifying an industrial-grade protocol has traditionally required five math PhDs working for two years, costing millions of dollars. Astra crushes that cost to roughly one percent. That's not a 30% or 50% efficiency gain — that's a complete restructuring of cost structures.
Consider what this means. The bottleneck in mathematical research was never "not enough smart people" — the number of top-tier mathematicians is extremely limited, and a Fields Medal-worthy result might take a genius a decade. But if AI can reduce the cost of proof from "a rare genius's decade of life" to "$2,000 in compute," the production bottleneck shifts from human brains to compute. This won't replace mathematicians; it gives every mathematician an army of tireless graduate students.
"Formal verification used to be too expensive for widespread use — proving an industrial protocol might take five PhDs two years. Models like Astra can push that cost down to one percent. This is the end of math's 'pre-Claude Code era.'"— Ma Xiao, Mathematics Researcher, University of Michigan
The more immediate impact is in software engineering. Formal verification has long been the gold standard for software correctness — mathematically proving code has no bugs — but because of cost, it's barely used outside aerospace, cryptographic protocols, and chip design. If AI can bring formal proof costs down to thousands of dollars, critical software systems — OS kernels, crypto libraries, smart contracts, even AI safety constraints — could be mathematically proven correct.
This is not science fiction. Several of Astra's 10 problems concern arithmetic circuit complexity and lattice cryptography — foundational problems in computer science and cryptography. An AI that can prove mathematical theorems can prove code correctness, prove encryption scheme security, even prove that AI systems behave within intended bounds.
What Astra Is: A Multi-Agent System, Not a Chatbot
From available information, Astra is not a single large model but a multi-agent collaborative system.
It works more like a math research team: agents understand problems and survey literature, agents propose proof strategies, agents translate strategies into Lean code, agents check for gaps, agents fix errors. Multiple agents iterate within a collaborative framework until a complete, machine-verifiable proof emerges. The process mirrors how human mathematicians do research — formulating conjectures, attempting proofs, discovering gaps, revising approaches, reaching final form.
Notably, OpenAI's timing in revealing Astra resonates subtly with Sam Altman's recent Washington activities. The same week Astra launched, Altman visited the White House to preview GPT-6 (internal codename) for members of Congress, as the U.S. government develops frontier AI regulation frameworks. A breakthrough like AI solving math problems — the kind of achievement that reads as "national prestige" — is far more compelling in policy conversations than "we built another stronger chatbot."
Of course, Astra's limitations deserve a cool-eyed assessment. These 10 problems concentrate in areas of mathematics where rules are explicit and answers are formally verifiable — precisely where current AI excels: symbolic reasoning, logical deduction, searching within well-defined spaces. Whether AI can be equally effective in mathematics requiring intuitive leaps, cross-domain associations, or physical-world modeling (geometric topology, mathematical physics) remains an open question. You can't expect a robot that can barely grasp a cup to prove the Riemann Hypothesis tomorrow.
The Tipping Point from Tool to Originator
Pull back the timeline, and Astra represents a genuine watershed.
Every previous AI capability demonstration — writing code, translation, image generation, writing, even discovering new antibiotics — was essentially executing tasks humans had already defined. AI did them faster and cheaper, but humans drew the boundaries, set the evaluation criteria, and the outputs lived within the known universe. GPT-4 in 2023 could pass the bar exam, but it didn't invent new legal theories; Claude in 2024 could write code, but it didn't invent new algorithmic paradigms.
Astra is different. It solved problems humans had not solved, and the proofs are independently verifiable. This is a critical step from "executing known tasks" to "exploring unknown territory."
The implications may unfold at three levels:
First, accelerated research in math and theoretical CS. If proving is cheap enough, mathematicians can focus on asking good questions and building grand frameworks, leaving tedious proof details to AI. Just as calculators didn't put mathematicians out of work but let them study more complex problems.
Second, formal verification moves from luxury to commodity. When proving system correctness costs thousands rather than millions, critical infrastructure software, financial systems, and AI safety constraints can all be mathematically verified. This may be one of the most important technical paths for AI safety — not making AI "ethical," but mathematically proving its behavioral bounds.
Third, AI-accelerated AI research. If AI can prove mathematical theorems, it can prove new algorithm correctness, optimize mathematical properties of model architectures, even design more efficient neural network structures. That's a recursive self-improvement loop — AI helping improve AI, faster and faster.
There is, of course, a philosophical question: if an AI proves a theorem but no human can fully comprehend the proof (because it's too long and complex), who does the proof belong to? Some of Astra's proofs may already approach this boundary — humans can verify each line of Lean is correct, but the overall proof's "idea" might exceed a single brain's grasp. This isn't new in math — the 1976 computer proof of the Four-Color Theorem sparked similar debate — but AI pushes the problem to an unprecedented scale.
$2,000. Next time you open ChatGPT or Claude to chat, remember that number. Behind every token you type, it's not just servers consuming electricity — there's a fast-growing "AI mathematician" that, for the price of a laptop, produced mathematical discoveries humans couldn't reach in decades. Mathematics is the queen of sciences; formal verification is the foundation of engineering. When both are conquered by AI at rock-bottom cost, the entire paradigm of research and engineering gets rewritten.
See you tomorrow.
OpenAI Astra · 数学证明 · Lean形式化验证 · 2000美元算力 · 非sofic群 · Erdős猜想 · 多智能体系统 · AI科研 · 形式化验证民主化 · Timothy Gowers
OpenAI Astra · mathematical proofs · Lean formal verification · $2000 compute · non-sofic group · Erdős conjecture · multi-agent systems · AI research · formal verification democratization · Timothy Gowers
