OpenAI 公布三项基础问题证明：局部平滑化、ETH 反证与杨-米尔斯存在性

• 发布内容：OpenAI 称其模型在数学、计算复杂性理论和量子场论三个方向生成证明，分别为所有维度的局部平滑化猜想、指数时间假设（ETH）的反证，以及四维相互作用量子场论的存在性证明。
• 数学结果：模型于 10 月 18 日生成局部平滑化猜想的自然语言证明，次日完成 Lean 形式化。OpenAI 称该猜想可推导出所有维度的卡凯亚猜想与 Stein 限制性猜想；此前王虹与 Joshua Zahl 在 2025 年证明三维卡凯亚猜想。
• 计算机科学结果：模型于 10 月 16 日生成 ETH 反证，次日完成 Lean 形式化。ETH 原始提出者 Russell Impagliazzo、Ramamohan Paturi 与 MIT 的 Ryan Williams 将领导外部团队审查；OpenAI 同意公开原始数据并资助学术会议。
• 物理结果：模型于 9 月 9 日和 9 月 18 日分别生成杨-米尔斯存在性与量子色动力学相关证明，10 月 16 日完成前者 Lean 形式化。2004 年诺贝尔物理学奖得主 David Gross 领衔五人团队审查，原始材料暂不公开。
• 发布策略与边界：10 月 6 日 OpenAI 曾公开 722 份 AI 生成数学手稿，涉及 372 个未解决问题，后撤回 3 篇并修订 14 篇。本次将证明视为原始研究数据，邀请外部科学家验证，且不寻求学术署名。上述结果来自 OpenAI 的发布材料，尚待外部团队审查与学界复现。
• 行业意义：生成证明与形式化检查正在把瓶颈推向“验证、解释与消化”。Lean 形式化能检查证明步骤，但不等同于数学界对结果重要性和正确性的全面确认。

🔗 爱范儿报道