OpenAI Astra 解 10 个数学难题：AI 科学突破为什么必须带 Lean 证书？

OpenAI 8 月 1 日发布的 “Ten advances in mathematics and theoretical computer science”，是这几天最重的 AI 科学信号。它不适合写成“AI 已经取代数学家”的夸张标题，更适合认真看：当前沿模型开始产出科研结果，什么样的证据链才足够让共同体讨论？

OpenAI 披露，内部版本的 Astra 模型在 10 个数学和理论计算机科学长期问题上给出了结果或实质进展。领域包括高维 sphere packing、binary and spherical codes、non-sofic groups、Connes rigidity conjecture、arithmetic circuit complexity、quantum parallel repetition、closest vector problem、Ehrhart volume conjecture、multicolor Ramsey numbers 和 extremal graph theory。

这些词听起来很远，但真正值得写的不是每个问题本身，而是 OpenAI 选择的发布方式。

OpenAI 说，这些结果由内部 Astra 模型产生，按 Sol API 价格估算，寻找解法所需 token 总成本约 2000 美元。随后，人类用同一个模型把论证整理成 manuscript，并由模型把每个论证形式化成 Lean certificate。OpenAI 还为每个解法发布了模型对思考过程的叙述。

这是一种新的科研生产链条：模型探索，模型叙述，人类整理，Lean 验证，社区复核。

为什么 Lean certificate 重要？因为数学和很多自然语言任务不同。一个回答看起来像证明，不代表它就是证明。大模型特别擅长写出流畅、像真的、局部合理的论证文本。要把 AI 生成的数学结果拿到严肃共同体里讨论，就必须有机器可检查的形式化层，至少让人知道“这个逻辑链是否真的闭合”。

这也是 AI 科学和普通 benchmark 的区别。Benchmark 可以给一个分数，数学结果必须经得起复现、审稿、引用和反驳。OpenAI 这次没有只发宣传稿，而是提供 paper、Lean formalizations 和 reasoning walkthroughs，这比单纯声称“模型解决了问题”负责任得多。

但谨慎也很必要。OpenAI 自己也承认，AI 能参与数学研究带来的问题不能由一家技术公司独自回答。AI 生成证明的署名怎么处理？未公开 reasoning trace 和 prompts 是否足够透明？Lean 形式化能覆盖哪些隐含假设？数学共同体如何判断一个结果的意义，而不只是正确性？这些都不是工程团队能单方面拍板的。

这篇文章里还有一个容易被忽略的点：OpenAI 说人类帮助准备 manuscripts 和 Lean formalization，并对正确性负责，但数学论证本身由系统生成。这种归因方式很微妙，也可能成为未来 AI 科学论文的模板。作者不再只是“谁写了文字”，而要区分“谁提出想法、谁生成证明、谁形式化、谁验证、谁承担责任”。

对技术圈来说，Astra 这条线有三个启发：

• 科学 AI 的价值不只是回答问题，而是生成可验证对象。
• 形式化验证、Lean、proof assistant 会变得更重要。
• AI 研究结果必须有比“模型这么说”更硬的证据链。

我的判断是，未来 AI 科学突破会分成两类。一类是看起来很震撼但难以验证的自然语言结果，热度高但可信度有限；另一类是带代码、数据、实验协议、形式化证明或可复现实验的结果，传播慢一点，但更可能真正改变学科。

OpenAI Astra 这次的重点，不是宣布数学家过时，而是提醒我们：AI 进入严肃科学之后，验证基础设施会和模型能力一样重要。没有 Lean 证书的“数学突破”，以后会越来越难让人放心。

参考来源：OpenAI：Ten advances in mathematics and theoretical computer science。