OpenAI 数学成果落地:722 篇论文与 88 小时证明改写专家角色

shashib · x · 2026-11-03

OpenAI 近期公布的数学成果标志着「专家判断被移入 prompt」的转折:9 月其智能体以约 1 万个 agent 运行 88 小时产出纳维-斯托克斯千禧年大奖问题的证明,并用 Lean 定理证明器形式化;10 月 6 日又发布 722 篇 AI 撰写的手稿,覆盖数百个开放问题,其中 162 篇在发布时已用 Lean 形式化主结果。克雷数学研究所称该问题「显然已被解决」,专家评审仍在进行。

Rutgers 数学教授 Alex Kontorovich 在 Marketplace Tech 节目中指出,数学家与 AI 协作时精力集中在两件事:陈述问题与检验结果。作者将这一分工推广到企业团队:给 agent 写指令时同样需要为「出题」和「验题」两个环节都配备人力。文中还引 arXiv 2025 论文估算:每步准确率 99% 的 1000 步论证,整体存活概率仅 0.004%,凸显形式化验证的必要性。