首页 时政热点 科技头条 智能AI 安全攻防 数码硬件 开发者生态 汽车 游戏 社会热点 开源推荐 医疗健康 归档 标签 关于
智能AI morning

翻完OpenAI的722篇数学手稿,我们挑出了最重的30道名题

摘要

编辑|Panda 今天上午,OpenAI 把一个尚未发布的内部模型产出的 722 篇数学手稿一次性放上了 GitHub。发布本身的来龙去脉、模型背景和数学界的争议,我们在 上一篇报道 里已经梳理过。这一篇换个角度,打开仓库,看看清单上到底有哪些成果。 仓库地址:https://github.com/openai/math 首先,有必要进行一些说明: 第一, 这 722 篇手稿被归入 372 个「成...

OpenAI 形式化 Lean BSD Goldfeld 722 准黎曼猜想 zeta 006 卡塔兰常数
2026-10-08 1 阅读 约10分钟阅读 机器之心
分享:
字号:
编辑|Panda 今天上午,OpenAI 把一个尚未发布的内部模型产出的 722 篇数学手稿一次性放上了 GitHub。发布本身的来龙去脉、模型背景和数学界的争议,我们在 上一篇报道 里已经梳理过。这一篇换个角度,打开仓库,看看清单上到底有哪些成果。 仓库地址:https://github.com/openai/math 首先,有必要进行一些说明: 第一, 这 722 篇手稿被归入 372 个「成果族」,覆盖数论、几何、理论计算机、数学物理等 17 个方向 ,本文按方向挑出其中名气最大、牵涉问题最古老的一批来介绍。 第二, 清单里既有「证明」也有「证伪」 ,按我们的粗略检索,摘要中出现「证伪」「反例」字样的成果族约有 50 个,一些流传了半个多世纪的猜想是被推翻而不是被证明的。 第三,也是最重要的一点:下文所有「证明了」「解决了」都是 OpenAI 自己的表述,绝大多数尚未经过同行评审。其中约六成成果族附有 Lean 形式化,即由计算机逐行检查过的证明,我们会在提到时注明; 没有 形式化 的结果,目前只能算「声称」 。 数论:从黎曼到希尔伯特 数论是这份清单里最惊人的部分,31 个成果族中有好几项直接挂着史上最著名的名字。 排在仓库第 003 号的 准黎曼猜想 ,是传播最广的之一。黎曼在 1859 年提出,zeta 函数的非平凡零点全部落在一条竖线上;这个终极目标太远,数学家退而求其次,希望至少证明某条竖线右边干干净净、一个零点都没有。一百多年里,这件事始终没有做成。OpenAI 声称把这条线划在了 7/8 的位置,对 zeta 函数和所有狄利克雷 L 函数同时成立,并附上了 Lean 形式化。 准黎曼猜想 与黎曼猜想同列千禧年大奖难题的 BSD 猜想 ,也出现在清单上。它讨论的是椭圆曲线上有理点的多少,与一个解析函数在某一点的行为之间存在精确对应。OpenAI 的第 002 和 006 号成果族合在一起,声称对每一条有理椭圆曲线,在它「几乎所有」的二次扭曲上都证明了完整的 BSD 公式;其中 006 号还顺带证明了数论学家 Dorian Goldfeld 在 1979 年提出的 Goldfeld 猜想。这两项都没有形式化。 BSD 公式 Goldfeld 猜想 第 004 号指向的是 1900 年 希尔伯特提出的 23 个问题中的第十个 。原问题问的是:有没有一种通用算法,能判断任意一个整系数多项式方程是否有整数解?1970 年,Yuri Matiyasevich 在前人工作基础上给出了否定回答。但如果把「整数解」换成「有理数解」,问题就悬置了半个多世纪。OpenAI 声称这一版本的答案同样是否定的,这一项同样没有形式化。 希尔伯特第十问题(有理数域) 还有两项结果,普通读者也能一眼看懂题面。 一是 卡塔兰常数 ,也就是 1 减 1/9 加 1/25 减 1/49 如此交替下去的那个和,它是不是无理数一直没人知道;OpenAI 声称它是。 卡塔兰常数 二是 圆周率 π 「有多难被分数逼近」 :此前数学家能证明的上界大约是 7.1,OpenAI 声称最优值恰好是 2,也就是说 π 在这件事上和「绝大多数」无理数一样普通。后者还顺带解决了一道趣味数学界流传多年的问题,即所谓 Flint Hills 级数是否收敛。这两项都附有 Lean 形式化。 π 的无理性测度 代数几何:霍奇猜想的一角,与有理性之谜 代数与复几何以 36 个成果族排在第三。这里最醒目的是第 032 号: 对所有复 CM 阿贝尔簇证明有理霍奇猜想 。霍奇猜想是千禧年大奖难题之一,大意是某些「拓扑上看起来像几何对象」的东西,一定真的能由代数方程切出来。CM 阿贝尔簇是一类对称性极强的特殊对象,远不是全部情形,但 OpenAI 称借助 James Milne 此前的定理,这一结果还能推出有限域上所有阿贝尔簇的 Tate 猜想。仓库 README 也特意注明,这一项没有走模型的标准流程,且目前没有形式化。 CM 阿贝尔簇霍奇猜想 另一项值得留意的是第 054 号。 三次四维簇能否被有理参数化 ,是代数几何里出了名的难题,Alexander Kuznetsov 曾提出一个用「范畴」语言判断的猜想。OpenAI 声称构造出了满足这一判据、却依然不能有理参数化的例子,从而推翻了该猜想。 三次四维簇(Kuznetsov 猜想反例) 再往抽象处走,清单里还有第 069 号的 量子几何朗兰兹对应 。2024 年,Dennis Gaitsgory 等人以近千页的系列论文证明了几何朗兰兹猜想,OpenAI 声称把其「量子」版本在无理参数下也做了出来。 量子几何朗兰兹 第 008 号则声称解决了关于 Grothendieck–Teichmüller 李代数结构的 Deligne–Drinfeld 猜想 ,并附有 Lean 形式化。 Deligne–Drinfeld 猜想 分析与几何:挂谷、马勒和一百年前的猜想 几何与分析方向的名题同样密集。 挂谷问题 (第 074 号)起源于 1917 年日本数学家挂谷宗一的一个小问题:一根针要在平面上转一整圈,最少需要扫过多大面积?它的高维版本演变成调和分析的核心难题之一。今年 7 月,王虹凭借与 Joshua Zahl 合作证明三维挂谷集合猜想获得菲尔兹奖;OpenAI 声称在此基础上更进一步, 证明了三维的更强版本和四维的维数猜想 。这一项没有形式化,也是最需要专家尽快审读的成果之一。 三维挂谷极大猜想 四维挂谷 马勒猜想 (第 087 号)由 Kurt Mahler 在 1939 年提出,问的是一个凸体与它的「对偶体」体积乘积最小能有多小,直到 2020 年才有日本数学家解决了三维对称情形。OpenAI 声称 在所有维数上 同 时解决了 对称 与非对称两个版本 ,并刻画了所有取到最小值的情形,附有 Lean 形式化。 马勒猜想(对称) 马勒猜想(一般凸体) 第 071 号回到了更古老的年代。1908 年, Paul Koebe 猜想 平面上任何区域都可以通过保角变换,变成边界全是圆或点的「圆域」 。OpenAI 声称解决了这一猜想的存在性部分,附有 Lean 形式化。 Koebe 圆域猜想 几何方向的其他亮点还包括: 任意黎曼度量下的高维球面都有无穷多条闭测地线 (第 345 号),以及 度量版 Blaschke 猜想 (第 344 号),这两项目前都没有形式化。 球面上无穷多闭测地线 度量 Blaschke 猜想 理论计算机:唯一游戏猜想落地 理论计算机科学是整个仓库里成果族最多的方向,一共 40 个。其中分量最重的是第 102 号: 唯一游戏猜想 。 这个猜想由 Subhash Khot 在 2002 年提出,Khot 后来因此获得 2014 年奈望林纳奖。它的意义在于,如果猜想成立,一大批经典优化问题,比如把图的顶点分成两组、让组间连边尽量多的 Max-Cut 问题,其「最好能近似到什么程度」都会被一锤定音。2018 年,Khot 与合作者证明了其较弱的「2 对 2」版本,但完整猜想一直悬而未决。 OpenAI 声称给出了完整证明,并直接推出 Max-Cut、顶点覆盖等问题的最优近似门槛 ,主结果附
这篇文章对您有帮助吗?

订阅66必读

每日精选科技资讯,直达你的邮箱