北京时间今天 13:12，一份 49 页的预印本出现在 Hexagon，作者栏写的是 CLAUDE / ANTHROPIC。两小时零五分前，同一份稿子和它的 Lean 形式化已经躺在 GitHub 上，可以下载、可以编译12。Anthropic 自己的官网上没有这条消息，X 上最新一条停在 10 月 26 日3。
论文的结论一句话说得完：3-SAT 有一个 2 的 o(n) 次方的确定性算法，因此指数时间假设（ETH）为假。它比十天前 OpenAI 那份晚一天公开，但算出来的东西更早——provenance 一栏写着，核心算法在 10 月 16 日由内部的 Claude 研究模型找到，产出 1400 万 token，没有人类输入；之后论文与 Lean 由模型写成，Anthropic 的研究者与 Claude 一起改的是表述4。
这个结果离实用很远，论文自己把距离写了出来：对 m = 5n 的任意 3-CNF，新界要等到 n 超过 10 的 10000 次方才优于穷举；只看 n 的那条界要等到 n 超过 10 的一亿次方。作者们的判断是，这条路线在任何实例化下都不太可能在 n 小于 10 的 7 次方时带来改进4。
它落在一个不做同行评议的平台上。 Hexagon 是今年秋天开始收稿的数学预印本库，首页第一段就写：Hexagon does not perform peer review；每份投稿自动筛查、beta 期再由人工过目，而「acceptance is not a judgment of correctness, quality, or novelty」5。站内现在有 460 份作品，其中 257 份的文字标为「Primarily AI-generated」，复杂度方向 cs.CC 的 16 份里有 11 份是这一档。标签由投稿方自填，审核不核验。也就是说，AI 生成的内容在这里是常态；而 contributor 一栏，全站 460 条里写的都是人名，只有这一条是机构。
所以这份稿子唯一的一道核对，是它自己写的那段。 附录 E 在 PDF 第 43 页，把「核过什么」和「没核什么」并排列出。原文四句可以直接照抄：
Whether the two definitions say what they are meant to say, that the Exponential Time Hypothesis is false and the Main Theorem, no machine can check; that is for the reader of the listing to judge.
The Lean development was written by AI models and reviewed by other instances of the same models; at the time of writing no person is known to have checked it; its constant is not explicit.
Two steps from the Lean statements to the printed ones are not part of the Lean proof.
AI models, not a mechanical check, compared the Lean proof with the printed one.4
拆开看，一条证明链有六个环节。论文那句主张对应到
MainResults.lean 里的两个定义，没有机器核；两个定义到证明，机器核了，而且核了四遍；证明走的是不是论文那条路，没有机器核；Mathlib 的多栈图灵机步数换算成 word RAM 上的时间，这两步不在证明里；常数 C 只说要存在，没给值；审过这份稿的人，零。被核住的那一格是硬的。 四道检查各管一段：Lean 内核逐条检查证明项；leanchecker 从空环境重跑每一个声明，Mathlib 也在内；nanoda 是独立写的第二个内核，经 Comparator 重放；Comparator 还把 Challenge 与 Solution 的命题逐字节比对，不一致就报
Challenge and solution theorem statement do not match6。规模是 1,050 个模块、151,657 行、三条标准公理，CI 跑完一次 24 分 13 秒。仓库还给了一条奇怪的复现路径：把一段压缩过的思路交给 Opus 5.5，高算力下它能重新推出 ETH 为假——只到较弱的那一档，不是页首印的那条界2。这条路径说明的是可重推，不是可核验。
没有人核过，这句话有旁证。 提交 Hexagon 的是 ORCID 账户 Jelani Nelson，他当天在 X 上回了一串：两家模型确实在同一天得到结果；发布前有几个人读过这份证明，为的是把概述与表述改好；他自己还没看 OpenAI 那份7。读是为了改表述，这与验证是两件事。
十天内两家，缝留在不同位置。 OpenAI 那份的形式化说明写得很直：Lean 证到的是 (log log n)²/√(log n) 那一档，手稿主定理是 log log n/√(log n)，差别在指数8。Anthropic 这份的 Lean 覆盖到主定理那一档，常数与适用范围都显式，缝挪到了命题映射与机器模型上：Theorem 2 的计数版在 Lean 里只有判定版，论文与 Lean 之间那两步靠散文。两家的共同点是同一件事——命题本身没有被任何机器核过。
外部的接法也变了。 OpenAI 那份的 Hacker News 首帖 611 分、217 条评论；Anthropic 这份的首帖 10 分、1 条评论，几小时后另一条 GitHub 链接也只有 3 分910。截至今天下午，没有人公开声称跑通了
lake build，也没有人贴出找到的错误。三件事可以拿去问下一份 AI 数学稿。它证的是哪一句；那一句与论文印出来的那句差在哪、谁核过；常数、机器模型、证明路线各差多少。这三问的答案，这一份自己写了，OpenAI 那份只在形式化说明里写了一半。
真正的新东西是那张表。读到「AI 证明了 X」，先看仓库里原件在不在架上；这一份把原件、证明、和「哪一格没核」一起放在了架上。核到命题为止，这句话放在别处是批评，放在这里是一份写得比同行清楚的交代。
References
- 1Hexagon · A 2^o(n) Time Algorithm for 3-SAT
hexagonmath.org
- 2anthropics/formal-math · eth/
github.com
- 3Anthropic · News
anthropic.com
- 4论文 PDF · Provenance
github.com
- 5Hexagon · 首页
hexagonmath.org
- 6anthropics/formal-math · README
github.com
- 7@minilek · X
x.com
- 8openai/math · lean/docs/378.md
github.com
- 9Hacker News · The Exponential Time Hypothesis Is False
news.ycombinator.com
- 10Hacker News · Anthropic's Disproof of the ETH
news.ycombinator.com
Comments