需要说明的是，这十道题是从多次尝试中筛选出的成功案例。
据 OpenAI 披露，模型在早期探索阶段存在大量失败，GPT-5.2 Pro 对 Erd s 问题的一次通过率仅 1%-2%。Astra 呈现的是 " 成功精选集 "，而非无差别的全面碾压。
即便如此，Astra 交出的成绩单仍然是一道分水岭：AI 已从 " 解已知答案的题 " 跨越为 " 产出人类也未知的原创证明 "。AI 不再是科研的 " 助手 "，而是科研的 " 参与者 "。此次重塑基础科学发现范式的不是单一技术突破，是形式化验证、多智能体协同与成本崩塌三股力量的交汇。
从 " 解题 " 到 " 发现 "
要理解 Astra 十题意味着什么，必须回溯 AI 数学能力的进化曲线。
2025 年 10 月，OpenAI 宣称 GPT-5 解决了十个 Erd s 问题，但随后被澄清—— GPT-5 所做的不是原创证明，而是文献搜索，在已有论文中找到了未被数据库收录的解答。AI 擅长检索，不证明 AI 擅长创造。
转折发生在 2026 年 1 月。软件工程师 Neel Somani 使用 GPT-5.2 Pro 在短时间内生成了一份 Erd s 问题 #397 的原创证明，经 Harmonic 的 Aristotle 系统完成 Lean 形式化验证，菲尔兹奖得主陶哲轩亲自确认该证明为此前文献中不存在的新论证。随后问题 #728 和 #729 也在此后数日内相继被攻克。
今年 5 月 20 日，OpenAI 内部通用推理模型推翻了平面单位距离问题的核心猜想，一个自 1946 年提出、近 80 年无人撼动的离散几何命题。AI 找到了一族反例，核心思路借用了代数数论领域的 Golod-Shafarevich 定理，实现了多项式级别的改进。菲尔兹奖得主 Tim Gowers 称之为 "AI 数学的里程碑 "。
从 GPT-5 的 " 查资料 " 到 GPT-5.2 的 " 原创三题 "，再到 5 月模型 " 推翻 80 年猜想 "，最后到 Astra 的 "2000 美元横扫十题 "，八个多月的时间，AI 完成了从 " 图书馆管理员 " 到 " 独立研究者 " 的跃迁。
多智能体协同：从 " 一人解题 " 到 " 团队作战 "
Astra 的核心不是参数规模更大，而是组织方式根本不同。据报道，Astra 可以让多个智能体协同工作，拆分复杂任务、分配子目标、相互校验，并在数小时甚至数天内持续推进。十个开放问题不是由一个模型一口气推导出来的，而是由一个协调者将问题拆解为子命题，分配给不同专长的子智能体并行执行，再由验证智能体筛选、合并、检查逻辑一致性。
这一流程与人类数学研究团队的组织方式高度同构。Anthropic 的 Managed Agents、OpenAI 的 Agents SDK、微软 Agent Framework 1.0、LangChain 的 supervisor-as-tool，四家主流厂商的共识是：让多个 AI 自由讨论不是最优方案，一个管理者分配任务、多个执行者交付结果才是。
全球共振：不止 OpenAI 一家
Astra 并非孤例。Google DeepMind 的 AlphaProof Nexus 自主解决了 9 个 Erd s 开放问题，其中最早一题已困扰学界 56 年，单题成本最低仅 7.5 美元。北京大学 AI4Math 团队采用双智能体框架（Rethlas+Archon）推翻 Anderson 猜想，完成国内首次由 AI 自主解决数学开放问题并完成大规模形式化验证，生成了约 19000 行 Lean 代码。Math Inc 的 Gauss 在 5 天内完成了 8 维（E8）情形的球堆积定理形式化，随后再用约一周完成 24 维（Leech 格）情形，总计产出约 20 万行 Lean 代码（经优化后），原人类团队估计剩余工作量需 6 个月。
此外，Anthropic、字节跳动 Seed-Prover、月之暗面 Kimina-Prover、DeepSeek-Prover-V2 等系统也在各自方向推进神经定理证明的自动化。形式化推理赛道已经形成全球性竞争格局。
如果说上述突破展示了 AI" 能做数学 " 的能力，那么下一个问题就是：我们如何信任 AI 产出的数学结果？这正是 Lean 形式化验证所要回答的。
信任锚点
如果没有 Lean，以上所有突破都缺少一个关键环节——可验证性。
Lean 是一种交互式定理证明器，由微软研究院开发，将数学证明写成可被计算机逐行检查的代码。不同于传统学术论文依赖同行评议的主观判断，Lean 验证是二进制的，要么编译通过，要么报错。一旦一个证明在 Lean 中 " 编译 " 成功，它就不需要人类相信它，它本身就是正确的。Astra 十项成果的 GitHub 仓库中 "sorry" 计数为零，意味着形式化证明中无任何步骤遗漏或未证。
大语言模型的 " 虚假推理 " 问题在科研场景中是一个不可忽视的风险：同行评议精力、复现预算、沿着错误方向继续深挖的研究周期，都可能被 " 看起来对 " 的 AI 生成论文无声吞噬。Lean 提供了独立于 AI 的 " 终极裁判 " 系统，人类不需要逐行审阅 AI 产出的数千行推理，只需确认 Lean 编译器通过了即可。
产业界已率先为形式化验证买单。在芯片验证领域，25 岁华人创业者洪乐潼创立的 Axiom Math，据公司披露其 AxiomProver 系统在 2025 年 12 月 Putnam 数学竞赛中获得满分 12/12 的成绩，公司于 2026 年 3 月以超 16 亿美元估值完成 2 亿美元 A 轮融资。在密码学领域，形式化验证正在被用于后量子密码原语的安全性证明。在生物医药领域，形式化推理框架向 " 靶点 - 疾病 " 因果链推演的迁移也已进入早期探索阶段。
据 Mines Paris PSL 官方数据，Lean 数学库 Mathlib 已积累约 210 万行代码、超 27 万条已形式化的定理。Meta 的 ATLAS 项目消耗 1830 亿 token，将 26 本数学教材翻译为 Lean 代码库。让机器自动检查 " 是不是对的 " 的能力，正在从增值功能变成基础设施。
形式化验证解决了 " 可信度 " 问题，但另一个更根本性的变化正在发生，科研的成本结构正在被重写。
成本崩塌：从百万美元到两百美元
2000 美元这个数字，是 Astra 故事中最具冲击力的细节，但需要明确的是，这仅指推理算力的边际成本，不包括模型训练（数亿美元级）、基础设施投资以及人类研究者的选题与验证时间。
即便如此，边际成本的下降幅度仍然惊人。传统数学研究中，一个 Erd s 级别的开放问题可能需要一位顶尖数学家耗费数年甚至数十年，背后是终身教职的薪资、研究经费、博士生培养费用，折算成本在百万美元量级以上。Astra 以 2000 美元攻克十题，平均每题 200 美元，约相当于一个初级软件工程师一周的工资。
这是成本结构的崩塌。
成本下行趋势同样值得关注。2026 年 5 月单位距离问题，推理成本约 1000 美元。2026 年 8 月 Astra 十题合计 2000 美元，平均每题 200 美元。同期 DeepMind AlphaProof Nexus 单题成本最低仅 7.5 美元。同代模型的推理优化、专用硬件普及、多智能体架构对 token 利用效率的提升，都将在 Astra 发布后继续压缩这个数字。
当解决一个前沿数学猜想的边际成本降到 200 美元以下，" 只有天才数学家才能做前沿数学 " 这个隐含前提开始松动。
密码学冲击波
成本下降最直接的连锁反应发生在密码学领域。7 月 28 日，Anthropic 披露 Claude Mythos Preview 在约 60 小时、10 万美元成本内，发现了 NIST 后量子签名候选算法 HAWK-256 的格结构对称性缺陷，将密钥恢复的理论工作量从 2 的 64 次方降至 2 的 38 次方。次日，HAWK 开发者宣布从 NIST 标准化进程中撤回该方案。
这不是量子计算机攻破 RSA，这是纯粹由 AI 推理能力驱动的密码分析，不需要量子比特，不需要超低温冷却。当多智能体系统能以 200 美元一题的边际成本求解开放数学问题时，密码学家面临的不再是 "AI 能不能找到漏洞 "，而是 " 低成本密码分析何时平民化 "。
科研预算结构重配
科研能耗正从实验密集型转向推理密集型。高校计算中心的采购清单将从 " 更多 GPU" 扩展为 " 更多能跑形式化推理管线的算力配额 "。OpenAI 于 7 月 29 日推出的 "ChatGPT 学术研究者计划 " 向十万名科学家免费提供前沿模型访问权限，承诺到 2027 年前投入 2.5 亿美元——表面上是公益，本质上是在下一代科研范式中抢占用户习惯。
成本的急剧下降正在将一个问题推向台前：当 AI 能够以极低成本产出数学成果时，数学家自身的存在价值又该如何定义？
科学家从 " 证明者 " 走向 " 提问者 "
6 月 2 日，国际数学联盟（IMU）正式背书《莱顿人工智能与数学宣言》。截至撰写时，该宣言已获超过 3000 人签署，陶哲轩称其为 " 必要框架 "，多位菲尔兹奖得主也已签署。《自然》杂志于 6 月 18 日发表社论全面支持，呼吁其他学科效仿。
宣言指出 AI 对数学的五大威胁：不可靠结果、归属缺失、依赖不平等、过度炒作、自主性丧失。OpenAI 在其 Astra 报告中回应了这些关切，承认 AI 有 " 贡献 "，既不是把 AI 当成无生命的工具，也不是赋予 AI 作者身份，而是把人类放在 " 最终承担责任 " 的位置。
AI 的边界与科学家的新定位
Astra 解决的是 " 证明一个长期猜想是否成立 " 的证明型突破。而 " 提出一个全新交叉方向、需要直觉跳跃的猜想 " 的概念型突破，依然是人类最稀缺的能力。不过，单位距离问题的突破也展示了 AI 超出预期的跨域联想能力，它将代数数论的 Golod-Shafarevich 理论应用于离散几何，这种跨学科联系被数学家 Arul Shankar 评价为 " 具备原创、精妙的独立思想 "。AI 的跨域联想能力正在快速进步。
随着 Astra 可以 200 美元一题解决开放难题，人类数学家的工作重心将从 " 产生证明 " 向上游迁移到 " 提出好问题 "。莱顿宣言的务实建议是：人类研究者选择问题、设定标准、批判想法、验证结果；AI 贡献广度、速度和并行探索能力。
陶哲轩在 2026 年初的演讲中判断："AI 将成为数学研究中值得信赖的合作者。"Tim Gowers 在 5 月 20 日当晚最初误以为 AI" 证明 " 了单位距离猜想，写道：" 如果 AI 能想出这样的证明，数学家的好日子可能很快就要结束了。" 但次日他得知 AI 是 " 推翻 " 了猜想（而非证明），明确表示 " 如释重负 "。这一细节折射出数学界对 AI 能力的复杂心态，既为其潜力震撼，又为其边界感到宽慰。
验证机制的递归困境
如果 Astra 能以每天几十个问题的速度产生候选解，当前人类同行评议体系根本消化不了这个流量。Lean 形式化验证提供了部分答案，但将自然语言证明翻译为 Lean 代码本身也需要成本。AI 辅助的自动形式化正在缩小这个差距，但远未达到即插即用的水平。
于是出现一个绕不过去的困境：要规模化验证 AI 产生的数学结果，我们需要 AI 来自动化验证过程——但这又回到了 " 谁来验证验证 AI 的 AI" 的递归问题。当 AI 产出速度是人类验证速度的百倍以上时，最终裁决权可能退化为抽样检查权，而系统性犯错的风险窗口始终存在。
2000 美元不是奥尔特曼在国会山抛出的营销数字，它是一道分水岭。在这条线的左边，科学发现是人类智力的专属领地，昂贵、缓慢、依赖天才的偶然出现。在这条线的右边，科学发现开始变成一种可以被工程化、被规模化、被定价的服务。
当一个数学猜想的边际解决成本降到 200 美元，它就不再是 " 科研 "，它变成了 " 查询 "，" 做科研 " 这件事本身的成本结构也正在被重新定义。从历史经验看，重新定义成本结构往往意味着产业变革的开始。
基础科学的前沿发现，不再是一件只有人类才能做的事。但 " 什么值得发现 "、" 发现之后如何理解 "、" 谁来为发现负责 "。这些问题，仍然只属于人类。（本文首发钛媒体 APP，作者 | 硅谷 Tech-news，编辑 | 焦燕）
