内容来源：https://www.quantamagazine.org/as-ai-closed-in-on-unique-games-proof-researchers-raced-to-beat-the-machines-20261007/

内容总结：

2026年9月11日清晨，麻省理工学院教授、唯一游戏猜想领域权威专家多尔·明泽收到朋友短信，询问他是否即将解决理论计算机科学中最著名的悬而未决问题之一。明泽起初以为这是玩笑，但随后越来越多消息涌入，传闻逐渐成形：刚宣布了流体行为重磅证明、震动数学界的人工智能公司OpenAI，据称已发现唯一游戏猜想的证明，可能随时公布。短信暗示，如果明泽手头有自己的成果，现在正是发布的时机。

唯一游戏猜想是计算复杂性理论中的标志性问题，该理论研究数学问题的内在难度。大致而言，它指出一个关于同时满足多个约束的问题可能极其困难，即使你愿意接受对最优解的糟糕近似。该猜想的证明还将自动意味着，当前用于解决许多看似无关问题的方法无法改进。研究人员将离计算难度的统一理论更近一步。

事实上，明泽并未证明唯一游戏猜想。但他和研究生费宇谋、王硕最近证明了一个密切相关问题的里程碑式结果。他们正在撰写论文——这一过程通常需要数月甚至更长——此时传闻开始流传。三人加紧完成草稿，以免被OpenAI的新闻发布抢了风头。三天后，他们以完整性优先于清晰性，在网上发布了一篇95页的论文，首页附有免责声明：“当前版本在数学上是完整的，但并非我们希望分享的形态。”

他们快速发表的决定很快被证明是正确的。10月6日，OpenAI宣布了唯一游戏猜想的证明，以及横跨数学多个领域的另外376项结果。研究人员对大量AI证明的反应，是近年来进展之后已变得熟悉的那种警觉与好奇交织。他们对明泽结果的反应则没那么矛盾。

“他在这个主题上发表了许多出色论文，”卡内基梅隆大学理论计算机科学家瑞安·奥唐奈说，“这是又一篇真正伟大的论文。”

基本满意

唯一游戏猜想和该团队新成果的核心问题，都涉及同时满足许多可能相互冲突的约束。类似问题在日常生活中也会出现：比如填写数独，或为婚礼安排座位。（你希望把朋友安排在一起，同时确保不和的客人分在不同桌——而且每桌都得坐满。）

精确求解约束满足问题可能很难甚至不可能。有时存在满足所有约束的解，但所有已知方法都慢得令人痛苦。或者约束可能相互冲突，完美解根本不存在。

在这些情况下，研究人员往往愿意接受满足部分而非全部约束的近似解。复杂性理论家想理解为什么寻找这些近似解有时容易有时困难。“大量工作致力于试图找出边界在哪里，”奥唐奈说。

唯一游戏猜想最早由复杂性理论家苏巴什·霍特在2002年他还是一名研究生时提出，与这一探索密切相关。它涉及一个关于被称为图的数学对象的特定约束满足问题，图是由称为边的线连接节点的网络。给定一个图，要求你用固定调色板为其节点着色。每条边附带一条规则，决定两端节点应是什么颜色。例如，某条边可能要求两个节点颜色相同。另一条边可能要求如果一个节点是红色，另一个必须是蓝色；如果一个节点是绿色，另一个必须是黄色。

这个着色问题的难度取决于图的布局、允许的颜色数量以及具体约束集。霍特感兴趣的是最优着色满足大多数但非全部约束的情况——比如99%的约束。找到这种近乎完美的着色很困难。直觉上，找到满足较小比例约束——1%甚至0.001%——的着色似乎更容易。

唯一游戏猜想认为这种直觉是错的。无论你愿意把标准放松多少，总会有一些情况，即使这些次优着色也难以找到。

唯一游戏猜想提出了一个惊人主张，但其真正价值在于与其他问题的联系。研究人员利用该猜想攻击关于泡沫几何和投票系统性质的看似无关问题。2008年，计算机科学家普拉萨德·拉加文德拉证明，如果该猜想为真，那么对于每个不存在完美解的约束满足问题，某一经典算法都是最佳策略。你无法通过利用具体问题的特殊性质做得更好。

然而该猜想有一个盲点。它只适用于最优解满足大多数约束的情况，如上述99%的情形。对于存在完美解——100%约束都能满足——的情况，它什么也没说。

霍特从一开始就认识到这一局限。为处理这些情况，他定义了唯一游戏问题的一个变体，称为2对1游戏问题，其中约束更宽松。在原问题中，为边一侧的节点着色后，另一侧的颜色只能有一种选择。在新版本中，他允许两种可能的颜色。

他猜想，对于这个问题，存在最优解满足所有约束、但仍难以找到满足任何极小比例约束的解的情况。这个较少为人所知的猜想的证明，还将蕴含关于许多不属于唯一游戏猜想范围的其他问题的结果。

在9月的论文中，明泽及其同事证明了霍特第二个猜想的一个轻微变体，其后果几乎相同。对明泽来说，这项工作历时七年。

一叠失败

2018年，还是研究生的明泽在一项著名成果中发挥主导作用，该成果标志着向证明霍特两个猜想迈出了第一个重大进展。但他的进展最终停滞。然后，在2025年，他与费宇谋和王硕讨论了2对1问题，两人刚完成研究生第一年，并结束了成果丰硕的首次合作。

“我给了他们两个问题选项，”明泽说，“他们足够勇敢，选了这个。”

要解决该猜想，三人需要建立一座从2对1问题到另一个难度已被充分理解的问题的数学桥梁。在明泽此前的工作中，建桥的第一步涉及将图着色问题转化为关于“纠错码”的问题，纠错码是一种编码消息的方法，使接收者能检测并修复传输错误。

几个月后，费和王找到了构建纠错码的一个有前景的新方法。但他们看不出如何将这些新代码与建桥所需的所有其他部分结合起来。

“看起来非常遥远，”明泽说，“你需要奇迹发生，所有星辰对齐。”

此后数月，星辰并未对齐。三人反复尝试、反复失败，但拼装这些部分感觉“就像试图把圆形和三角形拼进同一个拼图，”费说。然而他们从每次受挫中学到了东西。2026年4月，他们终于成功了。

“我们经历了五次失败，设法把这个[新代码]钉在它们上面，”明泽说，“然后它就奏效了。”

严格来说，明泽、费和汪证明的是霍特2对1游戏猜想的一个稍弱版本，其中每个约束有四种选择而非两种。但霍特原猜想的许多推论已可从4对1版本得出——最引人注目的是关于一个经典图着色问题难度的新结果，该问题比霍特的工作早数十年。在这个著名问题中，唯一的约束是相邻节点不能同色。复杂性理论家早已知道，在给定图可用三种颜色着色的情况下，这样的解可能极难找到。明泽、费和汪的新结果现在意味着，在这些情况下，无论允许你使用多少额外颜色，总会有反常的图仍然难以找到解。

“即使有整盒蜡笔你也做不到，”普林斯顿大学的马克·布拉弗曼说。计算机科学家数十年来一直试图证明这一结果——事实上，这正是最初促使霍特提出其图着色猜想的那些问题之一。

OpenAI的10月发布包含一个经Lean验证的2对1猜想证明，但那是AI生成的手稿，未经过任何人工编辑或独立专家评审。不过，为抢在OpenAI发布前而匆忙完成的9月4对1结果也并非完美。

“从第6节开始，字面上没有连接词，”明泽说——只有一连串不间断的定义和中间结果证明。“我们觉得有必要为此道歉。”

团队计划在充实完善后发布新版本论文。但在AI辅助写作日益普及的时代，这份明显未打磨的文本自有其魅力。正如奥唐奈所说：“他们用老派方式解决了问题，用头脑，用自己的手指写出来。”

成功的代价

然后是OpenAI的唯一游戏猜想证明，它一点也不老派。这是迄今为止理论计算机科学中AI生成证明最引人注目的例子——这还包括OpenAI同时发布的另外40个理论计算机科学证明。

研究人员需要消化的东西很多。“通过新闻稿发布数学对数学不太健康，”布拉弗曼在9月被问及即将到来的OpenAI公告传闻时说，“我们已经经历了很多不确定性和不愉快。”不过他指出，AI生成的该猜想证明可能为研究人员开辟新方向。如果他们能梳理出证明中的关键假设——对AI生成的证明来说这并不总是容易——他们或许能通过调整这些假设并探索结果如何变化来学到很多。“这不是‘一劳永逸’，”他说。

数学和理论计算机科学领域的一些研究人员已通过采用AI工具进行自己的研究来回应AI能力的快速进步。明泽则担心新工具正在改变研究过程。他的新成果的故事就是一个例证。“失败并知道为什么失败很有价值，”他说，“使用AI把这一切都抽走了。”

他还担心AI进展会阻止研究人员追求雄心勃勃的长期项目。

“你是人，对吧？你需要睡觉，需要吃饭，有情绪，”他说，“你不知道自己是否会被那家万亿美元公司抢发。”

中文翻译：

当AI逼近“唯一游戏”猜想的证明，研究人员争相跑赢机器

引言

2026年9月11日早晨，多爾·明澤收到一位朋友发来的短信，问他是否快要解决理论计算机科学中最著名的未解问题之一。明澤是麻省理工学院的教授，也是“唯一游戏”猜想领域的顶尖专家，起初他以为这是个玩笑。接着更多消息涌来，传言开始变得有鼻子有眼。人工智能公司OpenAI刚刚宣布了一项关于流体行为的重磅证明，在数学界掀起波澜，据称又发现了唯一游戏猜想的证明。他们可能随时公布结果。那些消息暗示，如果明澤手头有自己的成果要发表，现在就是时候了。

唯一游戏猜想是计算复杂性理论中的一个标志性问题，该理论研究数学问题的内在难度。粗略地说，它指出一个关于同时满足多个约束的问题可能极其困难，即使你愿意接受对最优解的糟糕近似。该猜想的证明还将自动意味着，当前用于解决许多看似无关问题的方法无法再改进。研究人员将朝着计算难度的统一理论迈出一大步。

事实上，明澤并没有证明唯一游戏猜想。但他和他的研究生费宇谋和王硕最近证明了一个里程碑式的成果，涉及一个密切相关的问题。他们正在撰写论文——这个过程通常需要数月甚至更久——这时传言开始流传。三人加紧完成草稿，以免被OpenAI的新闻发布会抢了风头。三天后，他们以完整性优先于可读性为原则，在网上发布了一篇95页的论文，第一页附有免责声明：“当前版本的手稿在数学上是完整的，但并非我们希望分享的形式。”

他们决定快速发表很快被证明是正确的。10月6日，OpenAI宣布了唯一游戏猜想的证明，以及横跨数学多个不同领域的另外376项成果。研究人员对大量AI证明的反应是警觉与好奇并存，这在近期进展之后已变得司空见惯。他们对明澤成果的反应则没那么矛盾。

“他在这个主题上发表了许多出色的论文，”卡内基梅隆大学的理论计算机科学家瑞安·奥唐奈说，“这是又一篇真正伟大的论文。”

大体满意

唯一游戏猜想和该团队新成果的核心问题，都涉及同时满足许多可能相互冲突的约束。类似的问题在日常生活中也会出现：比如填数独，或者为婚礼安排座位。（你希望把朋友安排在一起，同时确保合不来的客人被分到不同的桌子——而且每张桌子的座位都得坐满。）

精确求解约束满足问题可能很困难，甚至不可能。有时存在一个满足所有约束的解，但所有已知的求解方法都慢得令人痛苦。或者约束之间可能相互冲突，完美的解根本不存在。

在这些情况下，研究人员通常愿意接受满足部分而非全部约束的近似解。复杂性理论家想理解为什么寻找这些近似解有时容易有时困难。“大量工作致力于试图弄清楚边界在哪里，”奥唐奈说。

唯一游戏猜想最早由复杂性理论家苏巴什·科特在2002年的一篇论文中提出，当时他还是研究生，该猜想与这一探索密切相关。它涉及一个关于称为图的数学对象的特定约束满足问题，图是由称为边的线连接的节点网络。给定一个图，要求你用固定的调色板为其节点着色。每条边都附带一条规则，决定两端节点应该是什么颜色。例如，某条边可能要求两个节点颜色相同。另一条边可能要求如果一个节点是红色，另一个必须是蓝色；如果一个节点是绿色，另一个必须是黄色。

这个着色问题的难度取决于图的布局、允许的颜色数量以及具体的约束集合。科特感兴趣的是最优着色满足大部分但非全部约束的情况——比如99%的约束。找到这种近乎完美的着色是一项困难的任务。直觉上，找到一个满足较小比例约束——1%甚至0.001%——的着色似乎更容易。

唯一游戏猜想说这种直觉是错误的。无论你愿意把标准放宽到什么程度，总会有一些情况，即使这些次优的着色也很难找到。

唯一游戏猜想提出了一个惊人的论断，但它真正的价值在于与其他问题的联系。研究人员已经利用该猜想进攻关于泡沫几何和投票系统特性等看似无关的问题。2008年，计算机科学家普拉萨德·拉加文德拉证明了如果该猜想为真，那么对于所有不存在完美解的约束满足问题，某一种经典算法就是最佳策略。你无法通过利用特定问题的特殊性来做得更好。

然而该猜想有一个盲区。它只适用于最优解满足大部分约束的情况，比如上面99%的情况。它对存在完美解——即100%的约束都能被满足——的情况不置一词。

科特从一开始就认识到了这一局限。为了解决那些情况，他定义了唯一游戏问题的一个变体，称为2对1游戏问题，其中约束更宽松。在原问题中，为边一侧的节点着色后，另一侧的颜色只能有一种选择。在新版本中，他允许两种可能的颜色。

对于这个问题，他猜想，存在最优解满足所有约束的情况，但仍然很难找到一个满足任何极小比例约束的解。证明这个不太为人所知的猜想，也将推导出许多不属于唯一游戏猜想范畴的其他问题的结论。

在9月的论文中，明澤及其同事证明了科特第二个猜想的一个轻微变体，其结论几乎相同。对明澤来说，这项工作历时七年。

一叠失败

2018年，还是研究生的明澤在一项著名成果中发挥了主导作用，该成果标志着朝着证明科特两个猜想迈出了第一个重大进展。但他的进展最终停滞了。然后，在2025年，他与费和王讨论了2对1问题，两人刚读完研究生一年级，并完成了第一次富有成果的合作。

“我给了他们两个问题选项，”明澤说，“他们足够勇敢，选了这个。”

要解决这个猜想，三人需要搭建一座数学桥梁，从2对1问题通向另一个难度已被充分理解的问题。在明澤之前的工作中，搭建这座桥梁的第一步涉及将图着色问题转化为关于“纠错码”的问题，纠错码是一种编码消息的方法，使接收者能够检测并修复传输错误。

几个月后，费和王发现了一种有前景的新方法来构建纠错码。但他们看不出如何将这些新编码与搭建桥梁所需的所有其他部分结合起来。

“看起来非常遥远，”明澤说，“你需要奇迹发生，所有星星都对齐。”

在那之后的几个月里，星星并没有对齐。三人反复尝试证明，反复失败，但拼凑各个部分感觉“就像试图把圆形和三角形拼在一起放进拼图里，”费说。然而他们从每一次受挫的尝试中都学到了东西。2026年4月，他们终于成功了。

“我们经历了五次失败，然后设法把这个[新编码]钉在它们上面，”明澤说，“然后它就奏效了。”

严格来说，明澤、费和王证明的是科特2对1游戏猜想的一个稍弱的版本，其中每个约束有四种选择而非两种。但科特原猜想的许多推论已经从4对1版本中得出——最引人注目的是，一个关于经典图着色问题难度的新结果，该问题比科特的工作早了几十年。在这个著名问题中，唯一的约束是相邻节点不能有相同颜色。复杂性理论家早就知道，在能用三种颜色为给定图着色的情况下，这样的解可能极其难以找到。明澤、费和王的新结果现在进一步表明，在这些情况下，无论你被允许使用多少额外颜色，总会有一些反常的图，仍然很难找到解。

“即使你有一整盒蜡笔也做不到，”普林斯顿大学的马克·布拉弗曼说。计算机科学家几十年来一直试图证明这一结果——事实上，这正是最初促使科特提出其图着色猜想的问题之一。

OpenAI在10月发布的成果包含了一个经过Lean验证的2对1猜想证明，但这是一份AI生成的手稿，没有经过任何人工编辑或独立专家审查。倒不是说9月的4对1成果就完美无缺——那份论文是为了抢在OpenAI发布之前匆忙完成的。

“从第6节开始，字面上没有任何连接词，”明澤说——只是一连串不间断的定义和中间结果的证明。“我们觉得有必要为此道歉。”

团队计划在完成充实后发布论文的新版本。但在AI辅助写作日益普及的时代，这份明显未经润色的文本自有其魅力。正如奥唐奈所说：“他们用老派的方式解决了问题，用他们的头脑，用他们自己的手指写出来。”

成功的代价

然后是OpenAI对唯一游戏猜想的证明，这一点也不老派。这是迄今为止理论计算机科学中AI生成证明最引人注目的例子——这还包括OpenAI同时发布的另外40个理论计算机科学证明。

研究人员需要消化的东西很多。“通过新闻稿做数学对数学来说不太健康，”布拉弗曼在9月被问及即将到来的OpenAI公告传言时说，“我们已经经历了大量的不确定性和不愉快。”不过，他指出，AI生成的该猜想证明可能为研究人员开辟新的探索方向。如果他们能梳理出证明中的关键假设——对于AI生成的证明来说，这并不总是容易的事——他们或许能通过调整这些假设并探索结果如何变化来学到很多。“这不是‘一锤子买卖’，”他说。

数学和理论计算机科学界的一些研究人员通过采用AI工具来进行自己的研究，以应对AI能力的快速进步。明澤则对新技术如何改变研究过程感到担忧。他的新成果的故事就是一个例证。“失败并知道为什么失败有很大的价值，”他说，“使用AI把这一切都拿走了。”

他还担心AI的进步会让研究人员不愿追求雄心勃勃的长期项目。

“你是人类，对吧？你需要睡觉，需要吃饭，你有情绪，”他说，“你不知道自己会不会被那家万亿美元的公司抢发。”

英文来源：

As AI Closed In on ‘Unique Games’ Proof, Researchers Raced to Beat the Machines
Introduction
On the morning of September 11, 2026, Dor Minzer received a text message from a friend asking whether he was close to settling one of the most famous open questions in theoretical computer science. Minzer, a professor at the Massachusetts Institute of Technology and a leading expert on the “unique games” conjecture, initially thought it was a joke. Then more messages started coming in, and the rumors began to cohere. The artificial intelligence company OpenAI, fresh from announcing a bombshell proof about the behavior of fluids that sent ripples through the math world, had allegedly discovered a proof of the unique games conjecture. They might make the result public any day. If Minzer had any results of his own to share, the messages suggested, now would be the time to do so.
The unique games conjecture is an iconic question in computational complexity theory, the study of the inherent difficulty of mathematical problems. Roughly speaking, it states that a problem about satisfying multiple constraints at the same time can be extremely hard, even if you’re willing to settle for a poor approximation of the best possible solution. A proof of the conjecture would also automatically imply that current methods for solving many seemingly unrelated problems can’t be improved. Researchers would be a big step closer to a unified theory of computational difficulty.
Minzer had not, in fact, proved the unique games conjecture. But he and his graduate students Yumou Fei and Shuo Wang had recently proved a milestone result about a closely related question. They were in the midst of writing up their findings — a process that would typically take months or longer — when the rumors began circulating. The trio rushed to finish their draft to avoid being overshadowed by an OpenAI press release. Three days later, prioritizing completeness over clarity, they posted a 95-page paper online with a disclaimer on the first page: “The current version of the manuscript is complete mathematically, but it is not in the shape we wished to share in.”
Their decision to publish quickly was soon vindicated. On October 6, OpenAI announced a proof of the unique games conjecture, along with 376 other results across many different fields of math. Researchers greeted the deluge of AI proofs with the mixture of alarm and curiosity that has become familiar in the wake of recent advances. Their reaction to Minzer’s result was less ambivalent.
“He’s put out many great papers on this topic,” said Ryan O’Donnell, a theoretical computer scientist at Carnegie Mellon University. “This is another truly great one.”
Mostly Satisfied
The problems at the heart of both the unique games conjecture and the team’s new result are about simultaneously satisfying many constraints that may be in tension with each other. Similar problems arise in everyday life: filling in a sudoku puzzle, for instance, or planning seating arrangements for a wedding. (You’ll want to seat friends together, while making sure that guests who don’t get along are assigned to different tables — and you’ll have to fill all the seats at each table.)
Solving constraint satisfaction problems exactly can be hard or even impossible. Sometimes, there is a solution that satisfies every constraint, but all known methods for finding that solution are painfully slow. Or the constraints might conflict with each other, and a perfect solution simply doesn’t exist.
In these cases, researchers are often willing to settle for approximate solutions that satisfy some but not all of the constraints. Complexity theorists want to understand why it’s sometimes easy and sometimes hard to find these approximate solutions. “A lot of work has been devoted to trying to figure out where is the boundary,” O’Donnell said.
The unique games conjecture, first articulated in a 2002 paper by the complexity theorist Subhash Khot when he was still a graduate student, is intimately connected to that quest. It concerns a specific constraint satisfaction problem about mathematical objects called graphs, which are networks of nodes connected by lines called edges. You’re given a graph and asked to color its nodes using a fixed color palette. Each edge comes with a rule that determines what color the nodes at either end should be. For instance, one particular edge might require that the two nodes have the same color. Another edge might demand that if one node is red, the other must be blue, and that if one node is green, the other must be yellow.
The difficulty of this coloring problem will depend on the layout of the graph, the number of allowed colors, and the specific set of constraints. Khot was interested in cases where the best possible coloring satisfies most but not all of the constraints — say, 99% of them. Finding this near-perfect coloring is a difficult task. Intuitively it would seem easier to find a coloring that satisfies a smaller fraction of the constraints — 1% or even 0.001% of them.
The unique games conjecture says that this intuition is wrong. No matter how much you’re willing to relax your standards, there will always be cases where even these subpar colorings are hard to find.
The unique games conjecture makes a striking claim, but its real value lies in its connections to other problems. Researchers have used the conjecture to attack apparently unrelated questions about the geometry of foams and the properties of voting systems. And in 2008, the computer scientist Prasad Raghavendra proved that if the conjecture is true, one particular classic algorithm is the best strategy for every constraint satisfaction problem where no perfect solution exists. You can’t do better by exploiting the quirks of specific problems.
Yet the conjecture has a blind spot. It only applies to cases where the best possible solution satisfies most constraints, such as the 99% case above. It says nothing about cases where there’s a perfect solution — where 100% of the constraints can be satisfied.
Khot recognized this limitation from the beginning. To address those cases, he defined a variant of the unique games problem called the 2-to-1 games problem, in which the constraints are looser. In the original problem, coloring a node on one side of an edge must leave only one option for the color on the other side. In the new version, he allowed for two possible colors.
For this problem, he conjectured, there are cases where the best possible solution satisfies all constraints, but it’s still hard to find a solution that satisfies any tiny fraction. A proof of this lesser-known conjecture would also imply results about a host of other problems that don’t fall under the umbrella of the unique games conjecture.
In their paper from September, Minzer and his colleagues proved a slight variant of Khot’s second conjecture that has nearly the same consequences. For Minzer, the work was seven years in the making.
A Stack of Failures
In 2018, while still a graduate student, Minzer played a leading role in a celebrated result marking the first significant advance toward proving Khot’s two conjectures. But his progress eventually stalled. Then, in 2025, he discussed the 2-to-1 problem with Fei and Wang, who had just finished their first year of graduate school and wrapped up a fruitful first collaboration.
“I gave them two options of which problem to choose,” Minzer said. “They were brave enough to choose this one.”
To settle the conjecture, the trio would need to build a mathematical bridge from the 2-to-1 problem to another problem whose difficulty was already well understood. In Minzer’s previous work, the first step in building that bridge involved transforming the graph-coloring problem into a problem about “error-correcting codes,” a method for encoding messages so that a recipient can detect and fix transmission errors.
After a few months, Fei and Wang identified a promising new approach to building error-correcting codes. But they couldn’t see how to combine those new codes with all the other pieces that needed to go into the bridge.
“It looked very remote,” Minzer said. “You needed miracles to happen, all of the stars to align.”
For months after that, the stars did not align. The trio repeatedly tried and failed to make the proof work, but assembling the pieces felt “like trying to fit a circle and a triangle together in a jigsaw puzzle,” Fei said. Yet they learned something from each thwarted attempt. In April 2026, they finally succeeded.
“We took five failures and managed to staple this [new code] on top of them,” Minzer said. “And then it worked.”
Technically, Minzer, Fei, and Wang proved a slightly weaker version of Khot’s 2-to-1 games conjecture, in which there are four options for each constraint rather than two. But many of the implications of Khot’s original conjecture already followed from this 4-to-1 version — most notably, a new result about the difficulty of a classic graph-coloring problem that predates Khot’s work by decades. In this famous problem, the only constraint is that adjacent nodes can’t have the same color. Complexity theorists have long known that in cases where it’s possible to color a given graph with just three colors, such a solution can be prohibitively difficult to find. Minzer, Fei, and Wang’s new result now also implies that in these cases, no matter how many extra colors you’re allowed to use, there will always be perverse graphs where it’s still hard to find a solution.
“You cannot do it even with the entire Crayola box,” said Mark Braverman of Princeton University. Computer scientists had sought to prove this result for decades — in fact, it was one of the problems that originally motivated Khot to propose his graph-coloring conjectures.
OpenAI’s October release included a Lean-verified proof of the 2-to-1 conjecture, but in an AI-generated manuscript that didn’t undergo any human editing or review by independent experts. Not that the September 4-to-1 result, which was rushed to predate the OpenAI dump, is in perfect shape.
“From section 6 onward, there are literally no connecting words,” Minzer said — just an unbroken sequence of definitions and proofs of intermediate results. “We felt the need to apologize for that.”
The team plans to post a new version of their paper when they’ve finished fleshing it out. But in an age where AI-assisted writing is becoming increasingly ubiquitous, the distinctly unpolished text has its own charm. As O’Donnell put it, “They solved the problem in the old-fashioned way, with their minds, and wrote it with their own fingers.”
The Cost of Success
Then there’s OpenAI’s proof of the unique games conjecture, which is anything but old-fashioned. It’s the highest-profile example of an AI-generated proof in theoretical computer science to date — and that’s including the 40 other theoretical computer science proofs that OpenAI released at the same time.
It’s a lot for researchers to take in. “Math by press release is not that healthy for math,” Braverman said in September, when asked about the rumors of an upcoming OpenAI announcement. “There is a lot of uncertainty and unpleasantness that we already are experiencing.” Still, he noted, an AI-generated proof of the conjecture could open up new directions for researchers to pursue. If they can tease out the key assumptions in the proof — not always an easy task with AI-generated proofs — they might be able to learn a lot by tweaking those assumptions and exploring how the result changes. “It’s not ‘one and done,’” he said.
Some researchers in math and theoretical computer science have responded to the rapid advances in AI capabilities by adopting AI tools for their own research. Minzer, for his part, is concerned about how the new tools are changing the research process. The story of his new result is a case in point. “There is a lot of value in failing and knowing why you failed,” he said. “Using AI takes all of this out.”
He also worries about AI advances discouraging researchers from pursuing ambitious long-term projects.
“You are human, right? You need to sleep, you need to eat, you have moods,” he said. “You don’t know if you’re going to get scooped by the trillion-dollar company.”