AI科研范式革命：花200美元即可攻克一道数学世纪难题

OpenAI日前确认，其下一代模型Astra以约2000美元推理成本攻克了十道数学与理论计算机科学前沿难题，全部成果通过Lean形式化验证，代码开放在GitHub仓库中。这些难题涵盖高维球堆积、编码理论、群论、量子复杂性和极值组合学等多个领域，每道题学术积压均超十年。 需要说明的是，这十道题是从多次尝试中筛选出的成功案例。 据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完成了从“图书馆管理员”到“独立研究者”的跃迁。 AI数学能力进化时间线，从文献检索到独立发现，八个月完成角色跃迁 Astra的核心不是参数规模更大，而是组织方式根本不同。据报道，Astra可以让多个智能体协同工作，拆分复杂任务、分配子目标、相互校验，并在数小时甚至数天内持续推进。十个开放问题不是由一个模型一口气推导出来的，而是由一个协调者将问题拆解为子命题，分配给不同专长的子智能体并行执行，再由验证智能体筛选、合并、检查逻辑一致性。 这一流程与人类数学研究团队的组织方式高度同构。Anthropic的Managed Agents、OpenAI的Agents SDK、 微软 Agent Framework 1.0、LangChain的supervisor-as-tool，四家主流厂商的共识是：让多个AI自由讨论不是最优方案，一个管理者分配任务、多个执行者交付结果才是。 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轮融资。在密码学领域，形式化验证正在被用于后量子密码原语的安全性证明。在生物医药领域，形式化推理框架向“靶点-疾病”因果链推演的迁移也已进入早期探索阶段。 Lean形式化验证生态关键指标，Mathlib已积累超27万条已形式化定理 据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发布后继续压缩这个数字。 AI数学难题推理成本下降趋势，从单