https://github.com/openai/math
4小时前，OpenAI将一个尚未发布的内部模型产出的722篇数学手稿（372个成果组）整体公开至GitHub，含论文、源码和部分Lean形式化证明；模型共尝试约4000个问题，OpenAI自称平均每项成果算力约相当于ChatGPT Pro思考3小时。
手稿覆盖17个数学方向，声称在BSD猜想和霍奇猜想两道千禧年难题上取得部分进展：前者对Selmer余秩0或1的椭圆曲线给出完整公式，按密度覆盖绝大多数二次扭曲；后者覆盖CM阿贝尔簇全部维度及K3曲面乘积——均非完整解决。此外还声称攻克准黎曼猜想（ζ函数及狄利克雷L函数在Re(s)>7/8区域无零点）、有理数域上的希尔伯特第十问题（通用判定算法不存在）、π的无理性指数恰好为2、卡塔兰常数为无理数、唯一游戏猜想等重量级结果。
形式化验证进度不一：162篇论文的主结果已有机器可核验的Lean证明（含准黎曼猜想、Mahler猜想、Kaplansky猜想），其余约560篇尚无——π的无理性指数、希尔伯特第十问题等最抓眼球的成果恰在未形式化之列。OpenAI自己在仓库中提示，未形式化结果可能存在问题，并承诺持续补全。
[图片]
