一项尚未公开的 OpenAI 成果传闻，在 AI 证明可供审查前就改变了三名 MIT 研究者的发表计划。Dor Minzer 与博士生 Yumou Fei、Shuo Wang 于 9 月 11 日听说，公司即将发布 Unique Games 成果。9 月 14 日，他们贴出一份粗糙的 95 页论文，证明相关却不同的定理。OpenAI 于 10 月 6 日公布数学成果合集，其中包含声称证明 Unique Games 猜想的手稿。
这是一项科研事件，不只是 AI 排行榜成绩。人类团队的关键突破在 4 月已出现，当时仍在整理解释性手稿。邻近企业成果的预期，让建立公开优先权比完成阐释更紧迫。两项定理不互相替代，任何预印本出现也不能取代独立专家审查。
两项成果，而非同一证明的两个版本
Subhash Khot 于 2002 年提出 Unique Games。可以想象由边相连的顶点，每个顶点取一个标签。每条边有置换约束：知道一端标签，就唯一确定另一端可接受标签。一一对应正是“unique”的来源。
猜想涉及近似的计算困难性。通俗说，区分“几乎所有约束可满足”的实例与“只能满足极小比例”的实例很难。它不是说满足赋值不存在，而是讨论高效通用算法能对严格定义的输入族判断什么。
这影响优化：精确最优解过于昂贵时，研究者使用近似答案。Unique Games 将许多最佳已知近似保证与内在困难性相连。Raghavendra 于 2008 年的框架，在该猜想成立前提下，说明标准半定规划策略对广泛约束问题类别的最优性；方法先解几何松弛，再舍入为离散选择。
MIT 定理针对完美完备性，即初始实例的约束全部可满足，不只是几乎全部。在 2-to-1 游戏中，一个选定标签允许另一侧两个兼容选项；团队的 4-to-1 定理允许四个。它弱于原 2-to-1 主张，却达到通常 Unique Games 不直接覆盖的精确完备情形。
“全部”与“几乎全部”为何不同
Minzer 及合作者在 2018 年达到了近乎完美完备性。剩下一点差距，也可能阻止需要完全可满足起点的归约。因此达到精确端点不是修饰性改善。
Fei 和 Wang 于 2025 年开始与 Minzer 合作。较新的纠错码提供了有希望的要素，但与困难性归约其余部分的配合反复失败。4 月突破结合二次方程、中间验证层与采用 Grassmann 风格编码的内部验证器。
这些属于概率可验证证明技术：验证者随机抽查长编码证明的少量位置。困难性归约必须保留应接受与应拒绝实例之间的差距。构造的重要性在于层与层的互动，而不只是有一种编码。
一项推论涉及图着色：即便承诺图可用三色着色，用任意固定数量允许颜色找到有效着色，仍是 NP-hard。颜色更多，不必然得到高效通用方法。成果还影响某些超图的独立集问题；超图一条边可以连接两个以上顶点。
这不同于 OpenAI 对通常 Unique Games 猜想的主张。MIT 作者保护的是独立路线及推论，不是抢先发布公司手稿的复制品。
收到警讯三天后发布的代价
Minzer 团队说数学已完成，呈现形式却未达到期望。9 月 14 日 ECCC 预印本有 95 页，Minzer 称第六节后几乎没有衔接词：定义和中间证明仍在，但读者引导稀少。
阐释是科研基础设施的一部分。动机、过渡、比较与解释帮助他人核查构造并复用思想。团队可迅速建立时间戳，却仍欠共同体这部分工作。
他们不知道公司的论证、模型、确切主张和日程。因此，这不是遵循相似人类时间尺度的常规双团队竞赛。预期机器产出在专家判断前就重新分配了人类劳动。
OpenAI 发布带来第二个审查问题：规模
OpenAI 称内部模型尝试约 4,000 个问题，发布 722 篇手稿覆盖 377 个问题；其中一个合集有 40 份理论计算机科学证明。尝试、手稿、问题和证明是不同单位，不能混成“已解决问题数量”。
公司称每项结果的平均算力约等于 ChatGPT Pro 思考三小时。这不是 Unique Games 的精确成本，也不是每份证明相同预算。公司说约半数结果公告时已形式化；预计其余可形式化，属于未来判断。
Unique Games 手稿声称存在从 3SAT 到无权实例的显式确定性多项式时间归约，并有 Lean 形式化产物。它列出割、覆盖、排序、删除、聚类及约束满足问题推论。这些既依赖新定理，也依赖既有归约。
OpenAI 未将发布视为常规同行评审，并承认参考文献和阐释需要改进，表示支持理解重要生成成果。公开输出可以是重要证据，而不等于共同体已完成评价。
Lean 检验形式陈述，不回答所有科学问题
Lean 检查编码步骤能否由编码假设和规则推出，比模型自称文字正确强得多。但专家仍须比较形式定理与预期猜想、审查导入假设，并连接代码与手稿。
Unique Games 对量词顺序和字母表大小如何依赖误差参数敏感。依赖一变，看似相近的命题可能更弱。完备性、可靠性、显式性及多项式运行时间，都须符合标准复杂性主张。
通过检查的推导也不会自动说明关键思想、识别创新、正确归功前人或建立共识。验证与理解是相关阶段，不是同义词。仓促的人类论文同样需要专家细读和改进阐释，人类署名不会免除义务。
可复现性也分层。Lean 产物及依赖可用时，外部可复做检查；内部未具名模型不公开，部分摘要及汇总统计也没有提供全部提示、采样和人工干预。因此，复现验证不同于复现发现。
下一步关键是独立核对 OpenAI 主张的形式与含义、更清晰的 MIT 手稿，以及让机器规模产出可审查的发布实践。事件已改变研究者何时发表、如何保护优先权。能否更长久促进数学，取决于能否把可检查输出变成别人可以检验、改造和理解的解释。