bibibi.cc正在加载…
报道称OpenAI公开722篇AI数学手稿，部分附Lean证明，但整体尚未获独立背书。
OpenAI一口气放出722篇AI数学手稿，数学界开始验收
动察 Beating AI 快讯，OpenAI 公开了一批由未发布内部前沿模型产出的数学结果，共 722 篇手稿，来自约 4000 个开放研究问题的评测。不少手稿围绕同一个核心结果展开，合并后对应 372 组相互关联的结果。
其中几项直接碰到了长期未解决的重要问题。模型给出了 Unique Games 猜想的证明；证明黎曼 ζ 函数在实部大于 7/8 的区域没有零点，被称为「准黎曼猜想」；还处理了 CM 阿贝尔簇上的有理 Hodge 猜想，以及 1940 年代以来悬而未决的自由群因子问题。其中 Unique Games、准黎曼和自由群因子等结果已经附上 Lean 形式化证明，可以由计算机检查证明过程。
不过，这批结果还不能全部当成定论。OpenAI 表示，不同结果的验证程度并不一致，没有形式化证明的部分仍可能存在错误。参与发布咨询的独立数学顾问组 AGMAI 也明确表示，它没有为这些结果背书。
动察 Beating AI 快讯称，OpenAI公开了722篇由未发布内部前沿模型产出的数学手稿。
报道称，这批手稿来自对约4000个开放研究问题的评测，合并后对应372组相互关联的结果。
报道列出的结果涉及Unique Games猜想、黎曼ζ函数、CM阿贝尔簇上的有理Hodge猜想和自由群因子问题。
报道称，Unique Games、所谓“准黎曼”和自由群因子等结果附有Lean形式化证明。
OpenAI表示，不同结果的验证程度并不一致，没有形式化证明的部分仍可能存在错误。
独立数学顾问组AGMAI表示，它没有为这些结果背书。
以下为辅助分析，与已报道事实分开展示；重要信息请进一步核实。
这则快讯称，一个尚未发布的OpenAI内部模型生成了大量数学研究手稿。部分证明被写成Lean可检查的形式，但这只说明证明过程可以交给计算机检查，并不等于报道中的全部数学结果都已经获得数学界确认。
如果这些数学结果经严格审阅后成立，将展示AI处理开放数学问题和生成可形式化证明的能力；但原文已经说明各项结果的验证程度不同，因此目前更适合视为待验收成果。
新手应区分“模型提出证明”“Lean可检查”和“独立专家已确认”三个阶段；这篇快讯只明确表示部分结果有Lean形式化证明，并明确提到整体尚未获得背书。
正在加载事件时间线…