2026年10月7日，技术博主 Simon Willison 转载了一条在 Hacker News 引发震动的留言。图论研究者 Jake Boggan 看到 OpenAI 开源的数学库中赫然列着第 180 号问题，声称已经证明了巴内特猜想（Barnette's Conjecture）。 Boggan 早年在布达佩斯求学，断断续续为这道图论猜想倾注了 24年心血，面对突如其来的算法胜利，他留下了一句令人心酸的感叹：听到它被解决，感觉就像昔日的前女友在车祸中骤逝，心里空落落的。
这本是一场经典的算法碾压人类智力的悲情叙事，但事实的底色完全不同。翻开 OpenAI 存放在 GitHub 上的形式化验证文件 BarnetteHamiltonian.lean，在整份证明最关键的主定理末尾，赫然写着四个字母：sorry。在 Lean 交互式定理证明器中，sorry 并非谦逊致意，而是一个专门用来跳过未完步骤的占位符。这桩让数学界提前透支存在主义悲伤的机器神迹，根本没有通过形式化系统的内核校验。
撕开 180 号问题：一行 sorry 撑起的伪终结
巴内特猜想由 David W. Barnette 于 1969年 提出，是离散数学领域极为顽固的高峰。它断言所有有限简单 3-正则二部 3-连通平面图都存在哈密顿回路。半个世纪以来，学术界耗费海量算力，也仅仅把反例排查推演到了 86顶点 以下，宏观的全局证明始终悬在半空。
OpenAI 在数学目录第 180 号问题下挂出的论文题为《Paired states and Hamiltonian cycles in cubic bipartite planar graphs》，成文日期标注为 2026年9月24日。很多技术读者看到代码仓库中附带了 Lean 代码，便下意识认为该猜想已经被机器严格闭环攻破。然而计算机辅助证明有着绝对严苛的底线：要么全链条经由内核验证，要么等于没有证明。
-- OpenAI BarnetteHamiltonian.lean 核心片段
theorem barnette_conjecture (G : Graph) [PlanarEmbedding G]
[Bipartite G] [ThreeRegular G] [ThreeConnected G] :
HasHamiltonianCycle G := by
sorry代码中的 sorry 意味着模型仅仅形式化了命题本身的数学外壳，并将核心推导步骤强行留白。不仅如此，Lean 文件中自定义的图论概念是否与经典数学定义严格等价，同样未经任何推敲。
一个未经形式化检验的占位符，瞬间击碎了一位资深学者的心防。这暴露的不是人工智能的算力奇迹，而是当前科技传播中极度扭曲的认知鸿沟。
批发的未验证手稿：OpenAI 与 DeepMind 的分野
这次在 GitHub 抛出的成果并非单一孤例。根据官方说明，这批成果来自其内部未公开模型，一口气覆盖了约 4000个开放数学问题，抛出了 722篇手稿，划分为 372 个家族。OpenAI 自己在文档里留下了一条审慎的免责声明：成果处于不同验证阶段，可能存在错误。
这种把海量半成品推向公共领域的做法，与学术界的严谨范式大相径庭，也照出了顶尖实验室在技术路线上的明显断层。
两年前，DeepMind 的 AlphaProof 在 2024 年国际数学奥林匹克（IMO）中斩获银牌水平，拿下 28/42分。AlphaProof 之所以赢得学术界承认，在于它将题目严格转译为形式化逻辑，每一步状态转移都由交互式证明内核锁定，没有任何蒙混过关的容错空间。
相比之下，OpenAI 这次抛出的更像是一场粗线条的模型能力宣发。它避开了高难度的形式化逻辑闭环，直接让未公开模型批量吐出自然语言格式的论文手稿，并在代码仓库里用声明式接口充门面。这不仅没有解决历史猜想，反而制造了海量真假难辨的文献噪点。
- 提醒.不要把大模型生成的学术预印本与机器验证的数学定理混为一谈；缺少内核编译与同行评议的证明，本质上只是概率生成的推导草案。
算力重压下的学者：别为未完成的草稿过早哀悼
巴内特猜想之所以吸引几代学者前赴后继，源于它在图论史上的险峻地位。它的源头可追溯至 1884 年的 Tait 猜想，后者在 1946 年被 Tutte 构造出 46 个顶点的反例无情推翻。随后 Tutte 提出的二部图猜想又被 Horton 图打破。直到 1969 年，巴内特加上了平面性约束，才勉强收拢了现代二部图的边界。这道命题凝聚了人类在离散结构中对秩序的执着追问。
当人类研究者面对海量算力时，往往会产生一种心理代偿式的怯懦。看到大机构挂出代码与论文，便下意识地将解题权拱手让出，将几十年的学术生涯折算成被算法淘汰的悲凉。
人类数学家最沉重的代价，不是输给算力，而是被未经检验的算法草案打乱了呼吸。
对于纯数学界而言，眼下最真实的处境是审查成本的剧烈攀升。OpenAI 并没有把成果归功于任何具体的数学家，只是作为数据资产打包丢出。面对 722 篇鱼龙混杂的模型手稿，人类数学家不得不充当免费的清洗工，从动辄数百页的文本和带有 sorry 的代码里，逐行核查组合思想是否存在逻辑跳步。
接下来真正值得盯紧的变量只有两个：其一，数学界对 9月24日 手稿核心组合构造的同行评审能否挑出根本漏洞；其二，OpenAI 能否在其代码库的后续迭代中，真正把那行扎眼的 sorry 从 Lean 内核中抹除。在那一天到来之前，一切关于智力终结的自我悼亡，都未免太早了。