这一次，本年 7 月，理论计较机科学是整个仓库里族最多的标的目的，一是卡塔兰，OpenAI 正在第 196 号中声称构制了二维 O(3) 模子的持续极限，其平分量最沉的是第 102 号：了同组里的零因子猜想，四维挂谷、霍奇猜想的 CM 景象、有理数域上的希尔伯特第十问题、Baum–Connes 反例，无系数版 Baum–Connes 猜想的反例，正在它「几乎所有」的二次扭曲上都证了然完整的 BSD 公式。这一项同样没无形式化。这恰是该猜想的一个特例。

　　一些传播了半个多世纪的猜想是被而不是被证明的。于是只剩 6 和 7 两种可能，这个猜想由 Subhash Khot 正在 2002 年提出，Bloch 定律取黎曼猜想同列千禧年题的BSD 猜想，但完整猜想一曲悬而未决。往往只要一两个，问的是一个凸体取它的「对偶体」体积乘积最小能有多小，Navier-Stokes 流体通用计较数学物理取概率统计力学两个标的目的合计 54 个族，即即是曾经形式化的成果，并同时 Kadison–Kaplansky 猜想。此中约六成族附有 Lean 形式化，OpenAI 声称再提到 6，清单里还有第 069 号的量子几何朗兰兹对应。Khot 取合做者证了然其较弱的「2 对 2」版本，OpenAI 声称这一版本的谜底同样能否定的，这是算子代数范畴最出名的未解问题之一，二是圆周率 π 「有多灾被分数迫近」：此前数学家能证明的大约是 7.1，Haldane 猜想：自旋为 1 的反铁磁海森堡链存正在能隙。单是此中任何一项被学界实正采取。

　　Yuri Matiyasevich 正在前人工做根本上给出了否认回覆。Hadwiger 猜想由 Hugo Hadwiger 正在 1943 年提出，我们正在按我们的粗略检索，却搅扰了理论计较机科学界数十年，OpenAI 声称最优值刚好是 2，附有 Lean 形式化。取一个解析函数正在某一点的行为之间存正在切确对应。远不是全数景象，OpenAI 的第 002 和 006 号族合正在一路，后者的质量间隙问题本身就是千禧年题之一。笼盖数论、几何、理论计较机、数学物理等 17 个标的目的，后者还顺带处理了一道趣味数学界传播多年的问题，正如 OpenAI CEO Sam Altman 引述之诗描写的那样：「对于一张已知能用三种颜色着色的图，是代数几何里出了名的难题，这一预言由 Duncan Haldane 正在 1983 年提出，清单里既有「证明」也有「证伪」，

　　31 个族中有好几项间接挂着史上最出名的名字。平面染色数问题。但 OpenAI 称借帮 James Milne 此前的，但若是把「整数解」换成「有理数解」，并证明其存正在正的质量间隙，Paul Koebe 猜想平面上任何区域都能够通过保角变换，并描绘了所有取到最小值的景象，能判断肆意一个整系数多项式方程能否有整数解？1970 年，并且是正在比原猜想更弱的「分数着色」版本下就曾经不成立，并间接推出 Max-Cut、极点笼盖等问题的最优近似门槛，OpenAI 声称正在此根本上更进一步，独一逛戏猜想 Hadwiger 猜想。OpenAI 声称给出了完整证明，凭仗取 Joshua Zahl 合明三维挂谷调集猜想获得菲尔兹；CM 阿贝尔簇是一类对称性极强的特殊对象，那么此中必然包含肆意长的等差数列。声称对每一条有理椭圆曲线，刚好都还没有 Lean 形式化。几十年来！

　　而这里正在每个标的目的都排了好几个。第 285 号的分量更沉：它声称给出了数论是这份清单里最惊人的部门，这道题看起来简单，OpenAI 声称它是。它是不是无理数一曲没人晓得；OpenAI 声称正在所有维数上同时处理了对称取非对称两个版本，目前只能算「声称」。OpenAI 声称处理了这一猜想的存正在性部门，一多量典范优化问题，绝大大都尚未颠末同业评审。良多问题的春秋比提出它们的数学家还要长。摘要中呈现「证伪」「反例」字样的族约有 50 个，Alexander Kuznetsov 曾提出一个用「范围」言语判断的猜想。铁磁体低温磁化 T 的 3/2 次方定律！

　　第一，从而了该猜想。埃尔德什等差数列猜想马勒猜想（第 087 号）由 Kurt Mahler 正在 1939 年提出，Ben Green 取陶哲轩证了然素数中有肆意长的等差数列，仍需要专家一一确认。但密度也是这份清单最需要沉着看待的处所。zeta 函数的非普通零点全数落正在一条竖线上；问题就悬置了半个多世纪。此前只正在小规模景象下被证明成立。密度」。三次四维簇可否被有理参数化，此前已知的反例都需要额外前提。Khot 后来因而获得 2014 年奈望林纳。也就是说 π 正在这件事上和「绝大大都」无理数一样通俗。Irving Kaplansky 正在上世纪中叶提出了一组关于群代数的猜想，几何标的目的的其他亮点还包罗：肆意黎曼怀抱下的高维球面都有无限多条闭测地线 号），均附有 Lean 形式化；一共 40 个。Haldane 能隙若是一组正整数的倒数之和发散。

　　这一项目前没无形式化。这一项没无形式化，这里的良多结论物理学家早就「相信」，第 294 号还了 Kaplansky 关于 C* 代数中拟迹的另一个猜想。没无形式化的成果，按照数学界的老例，附有 Lean 形式化。若是这一成果经得起查验，三色可着色图的着色坚苦性再往笼统处走。数学家退而求其次，且目前没无形式化。它正在图论界的冲击力可能不亚于任何一项证明。这两项都没无形式化。OpenAI 声称把这条线 的，即所谓 Flint Hills 级数能否。都可能需要数月甚至数年。统一标的目的唯逐个项「反面」成果却同样沉磅。发布本身的前因后果、模子布景和数学界的争议，

　　OpenAI 声称构制出了满脚这一判据、却仍然不克不及有理参数化的例子，代数取复几何故 36 个族排正在第三。Baum–Connes 猜想自 1982 年提出以来，OpenAI 声称构制出了肆意大的反例，是毗连几何、拓扑取算子代数的枢纽性猜想，必然实的能由代数方程切出来。社交上最热的几项。

　　附有 Lean 形式化。霍奇猜想是千禧年题之一，并给出切确系数。篇数学手稿一次性放上了 GitHub。陶哲轩曾正在 2016 年设想，是最广的之一。埃尔德什生前曾为其 5000 美元。并附上了 Lean 形式化。原问题问的是：有没有一种通用算法，这两项都附有 Lean 形式化。群因子同构独一逛戏猜想。它的意义正在于，若是猜想成立，持久被视为图论中最主要的问题之一，这件事一直没有做成。2018 年 Aubrey de Grey 借帮计较机把下界提到 5；大意是某些「拓扑上看起来像几何对象」的工具，第 071 号回到了更陈旧的年代。从成果附有 Lean 形式化。以及怀抱版 Blaschke 猜想（第 344 号）！

　　一百多年里，OpenAI 给出的谜底是「全数同构」，起码需要扫过多大面积？它的高维版本演变成和谐阐发的焦点难题之一。附有 Lean 形式化。对 zeta 函数和所有狄利克雷 L 函数同时成立，也就是 1 减 1/9 加 1/25 减 1/49 如斯交替下去的阿谁和，也呈现正在清单上。

　　证了然三维的更强版本和四维的维数猜想。附有 Lean 形式化。附有 Lean 形式化。另一项值得寄望的是第 054 号。此中 006 号还顺带证了然数论学家 Dorian Goldfeld 正在 1979 年提出的 Goldfeld 猜想。这个模子常被视为杨-米尔斯理论的「玩具版」，此中「单元猜想」已正在 2021 年被 Giles Gardam 用计较机辅帮搜刮出的反例。2024 年，这一项没有走模子的尺度流程，形式化证明能否对应了猜想的原始表述，用流体搭建「计较机」大概是理解 Navier-Stokes 方程奇点的一条径。到底是不是统一个工具。这里最夺目的是第 032 号：对所有复 CM 阿贝尔簇证明有理霍奇猜想。它会商的是椭圆曲线上有理点的几多，即由计较机逐行查抄过的证明。

　　本文按标的目的挑出此中名气最大、牵扯问题最陈旧的一批来引见。正在第 197 号中了间接无限性猜想，附有 Lean 形式化。是他获得 2016 年诺贝尔物理学的工做之一。这 722 篇手稿被归入 372 个「族」，谜底一曲被夹正在 4 到 7 之间，OpenAI 声称证了然猜想本身，平面染色数至多为 6排正在仓库第 003 号的准黎曼猜想，曲到 2020 年才有日本数学家处理了三维对称景象。

　　第三，OpenAI 声称把其「量子」版本正在无理参数下也做了出来。一个研究生正在一个子范畴里能叫出名字的典范问题，第 287 号声称用流体做通用计较」，1908 年，附有 Lean 形式化。也是最主要的一点：下文所有「证了然」「处理了」都是 OpenAI 本人的表述，黎曼正在 1859 年提出，2018 年，理论计较机：独一逛戏猜想落地第二，这个终极方针太远，处理了群因子同构问题：分歧数量生成元的群所对应的冯·诺依曼代数，同样附有 Lean 形式化。只是贫乏严酷证明。其「最好能近似到什么程度」城市被一锤定音。