GPT-5.6 Sol Ultra 产生了周期双覆盖猜想的证明 [pdf]

证明有效性与验证

• 许多人感到兴奋但仍保持谨慎：这个证明很短，使用了 1990 年代之前的图论，看起来很有道理，但可能包含微妙错误。
• 有人认为，这样的结果应当由专业数学家宣布，或者至少在 Lean 形式化 / 期刊同行评审之后再宣布。
• 还有人指出，OpenAI 确实发布了一个 Lean 形式化仓库，但图论库仍不成熟，因此机械化并不容易。
• 几位评论者尝试让其他 LLM 和工具检查该证明；他们普遍表示没有发现明显错误，但强调这不能替代专家审查。
• Reddit 上提出的至少一个技术性担忧，在线程中被认为只是记号问题，而不是致命缺陷。总体结论：有前景，但尚未获得普遍接受。

提示词、执行框架与时间感知

• 发布的提示词带有很强的元指令性质：它要求模型假定存在一个证明，至少工作 8 小时，避免含糊的状态报告，并探索多种策略。
• 评论者将其视为“动机黑客”与元启发式指导，而非纯粹的自主性。
• 讨论涉及 agent harness 中的时间跟踪（时间戳、OS date、配额工具）与模型自身缺乏内在时间感之间的差异。
• Sol Ultra 被描述为许多并行的子代理并以最大推理运行，这与 Sol Pro 的“best-of-N”方法不同。

方法论的不透明与幸存者偏差

• 多位评论者询问：一共尝试了多少问题和提示变体？在这次成功之前有多少次失败运行？
• 有人推测，OpenAI 自先前的 unit-distance 结果之后就一直在跑很多问题；缺少“失败率”使得很难判断能力边界。
• 也有人担心，公司会把少数成功案例拿来营销，而把无结果的案例埋掉。

对数学与证明助手的意义

• 一些人认为这是一个重大里程碑：现成模型在不到一小时内解决了一个著名开放问题。
• 另一些人指出，这更像一种“巧妙技巧”式证明，而不是长篇、构建理论式的突破；他们认为下一道门槛是自主发展出实质性的新理论。
• 很多人强烈支持转向 Lean 风格的形式化验证，以应对海量 AI 生成证明，并减少人工检查的瓶颈。

更广泛的影响与焦虑

• 关于哪些任务最容易自动化的争论：任何正确性容易检查的领域（数学、代码、安全、部分科学）可能尤其脆弱。
• 关于纯数学价值的哲学讨论：AI 生成的结果是否“让人感觉空洞”，以及什么仍然是人类独有的（猜想生成、品味、解释、责任）。
• 一些人表达了对工作、人的价值以及 AI 炒作的担忧；另一些人回应说，人的价值并不与经济生产率绑定，工具会增强而不是抹去人类。