openai / math
其他
Lean
OpenAI 内部模型自动做数学研究的成果库,含 721 篇手稿与 Lean 形式化证明
这是 OpenAI 公开的一个数学研究成果库:用一个尚未发布的内部模型,对约 4000 个开放数学问题做自动研究,产出 721 篇手稿、归为 373 个主题族,涵盖数论、代数、概率、物理等多个方向,其中约 42% 的核心结果已用 Lean 完成形式化验证,其余部分仍可能存在错误。OpenAI 明确把这些成果定位为「原始研究数据」而非正式论文,部分结果附带模型推理过程的节选,比如 π 的无理数指数、Riemann zeta 函数零点区域、Kaplansky 猜想等。对读者来说,它的价值不在于直接使用,而在于观察 AI 做数学研究的真实上限:平均每题消耗约三小时 ChatGPT Pro 级别的思考算力,最终能产出什么量级的成果。值得看的是关注 AI for Science、推理模型能力边界的算法和研究岗位,以及对形式化证明(Lean)生态感兴趣的人;纯业务开发或不关心 AI 科研进展的读者关系不大。
★ 17k
24h +41
⑂ 1.9k
创建 29 天前
更新 6 天前