从糟糕的科幻到可机检的证明：一个门外汉用一个月撞开了 Conway 的猜想
把 10 拆成 2×5、21 拆成 3×7，再把 2 和 3 凑一堆、5 和 7 凑一堆，就得到 6 和 35。同一个 210，底下其实是四个数在重排。这件事对普通整数而言理所当然到不值得说。
拿 210 这个数。它可以拆成 10 乘以 21，也可以拆成 6 乘以 35。
把 10 拆成 2×5、21 拆成 3×7，再把 2 和 3 凑一堆、5 和 7 凑一堆，就得到 6 和 35。同一个 210，底下其实是四个数在重排。这件事对普通整数而言理所当然到不值得说。
John Conway 在 1976 年问的是：换成他自己的那套数，这件事还成立吗。
五十年前提出的这个问题，2026 年 9 月 18 日被人贴出了一份通过机械检查的 Lean 证明。贴出它的人叫 Dan Abramov，是一位软件开发者，在自己的文章里自称"数学小白"（math noob）【直引：Abramov 原文自述】。
🔢 什么数算"整数"
要理解这个猜想，得先认识超实数（surreal numbers）。
Conway 发明的这套数由一个规则长出来：把已有的数在数轴上摆好，在每两个相邻数的空隙里生成一个新数，"最左"和"最右"也算空隙。第一天只有一个空隙，生成 0。第二天有两个空隙，生成 -1 和 1。第三天生成 -2、-1/2、1/2、2。这样无穷无尽地长下去，实数、序数、以及各种古怪的组合都被装进同一棵二叉树。
超实数里的"整数部分"叫 omnific integers。它包含 3、-5 这类普通整数，也包含 ω、2ω、ω×ω、ω^ω、-ω/7 这些无穷大的家伙。在树上找它们的办法是看路径：只往左走、只往右走、或者只在无限次跳跃之后才改变方向一次。
Conway 精细化猜想（Conway's refinement conjecture）的内容是：如果 ab = cd，那么存在 e、f、g、h 使得 a = ef，b = gh，c = eg，d = fh。用前面 210 的例子说，就是任何两个因式分解都允许一个共同的精细化。
Conway 认为 omnific integers 有足够结构，能让普通整数的这条性质保住。这个问题一直开着，直到 L'Innocente 与 Mantova 的因式分解理论（*Advances in Mathematics*, 2024）把它归约成一个关于某类广义幂级数的问题：K((ℝ^≤0)) 中每个具无穷支撑的不可约元是否都是素元。选这个题目的时候，Abramov 从 Claude 那里得到的说法是"这个问题已被完美归约"。
他后来发现这句话是错的，真正证明需要的远不止那个归约【直引：Abramov 原文修正】。
🧪 五周，从一团乱麻到一台机器
整个项目用时一个月。过程比结果更有信息量，因为它把"用 AI 做数学"这件事的失败形态完整暴露了一遍。
第一周的做法最直白：把论文转成 TeX 喂给模型，让它直接攻这个猜想。产出被 Abramov 描述成糟糕的科幻小说，充满自造术语和戏剧化断言。
第二周他换了打法：把 Codex 下载到本地，搭出一个多角色实验室。角色包括项目经理、几个数学智能体、一个专门负责找缺陷的红队智能体、一个自由探索的随机智能体，以及负责把数学结论形式化成 Lean 的 Lean 智能体。关键是 Codex 的两个功能：Goals 会周期性提醒每个会话它的目标，防止跑偏；会话之间可以互相发消息。另有一个"食堂"智能体，把收到的每条消息转发给所有人，模拟群聊。
第一周那次探索最终留下了一个庞大的 TeX 文档和一堆 Lean 代码，没有证明猜想。
🔁 那个宣称"已解决"的夜晚
第三周有一次很典型的翻车。
ChatGPT 接近于宣布猜想已解，理由是一个名为 working_direct_cantor_bootstrap.md 的文件声称完整解决了问题。Abramov 让一个全新会话去攻它，几个小时后，新会话承认里面存在循环语句。ChatGPT 最终的裁定是"我们目前没有证明"【直引】。随后的检查发现，类似的逻辑缺陷也存在于更早的几份"论文"里，那些论文声称的结果因此全部作废。
那一周文档从十几篇膨胀到接近三十篇，任何一篇有错，后面的全部作废。Lean 形式化严重落后，一份自有新结果都没被认证过。
项目在那里停了一周。
🔥 "烧掉一切"救了这个项目
第四周回来时，Abramov 换了一个方向：不再攻猜想，先去查已有文献里的错误。
他做了两件事。一件是让模型梳理草稿，其中一个新会话的回答被原文引用："这个文件夹里目前没有任何文件给出了可信的 Conway 猜想证明……真正的失败是认识论上的——草稿制造了大量私有的定理文献，然后在其承重结果尚未被独立验证前就引用它们。"
另一件是给数学家发邮件求证模型指出的笔误。结论混杂：至少几处修正被确认为真；几处没有 Lean 支撑的问题经证实是误解；模型提出的几个"新颖"断言，数学家评价为正确但没有推进问题。
这一轮审计带来一个够强的新结果：主环的有限次数部分是多项式环。Abramov 与人类数学家确认了这个结果的新颖性，它随后在 Lean 中被认证。
Abramov 让模型自评产出结构，那个回答值得抄下来：约 10% 到 15% 含值得保留的数学，35% 到 45% 是正常数学但不构成贡献，40% 到 50% 是"bullshit"，即巨大的定理塔、自造标签，以及用进展口吻呈现的条件假设【直引：ChatGPT 自评，经 Abramov 转述】。
🧱 防漂移的那道墙
第五周的核心是审计基建。这里的设计思路可能是整个项目里最可迁移的部分。
配套的还有两个 Lean 智能体的分工。一个只负责认证底层前置论文；另一个认证新颖的 finite-degree 素性结果，在独立工作树里跑，被迫基于上游已认可的工作构建。后者的任务对前者保密。Abramov 的解释是：上一版实验室让同一个 Lean 智能体既认证前置论文又做半成品自有工作，导致不成熟的抽象与已被接受的数学纠缠在一起。
工具链方面，他用到了 Lean Comparator、TauCeti 的评审细则与公理检查器、Verso Blueprint，以及模块分层审计。
他还做了一件小事，对结果的可读性影响很大：在 Lean 源码里用一个特殊 attribute 标注"重要"定理，自动生成 Mermaid 证明结构图。
他的总结是：模型没法优化它看不见的东西。想要更简单的证明形状，就得让它"看见"形状；反过来，模型也没法忽略它看见的东西，不想要奇怪的术语就得把术语剥掉。
💸 一个月，四千亿 token
最后几天他从一次预发布模型的使用额度里获得了短暂的无上限访问。
模型分工上有一条被反复验证的观察：Claude 在有清晰无误目标时写 Lean 很擅长；ChatGPT 平均更擅长思考新数学，在协调与坚持目标上明显更好。Abramov 自己的答案是"两个都用"。
🚦 验证到了哪一步
这是全文最需要说清楚的部分。
| 项目 | 状态 |
|---|---|
| Palomar 注册表机械检查 | 通过，entry PALOMAR-2026-09-03-000002，version 1 |
| 熟悉 Lean 与该领域的人士 | 认为陈述看起来正确 |
| 数学家独立验证 | 未完成 |
| 作者态度 | 明确邀请反驳 |
| 前提 | 证明不依赖 Lean 内核的 bug |
Abramov 的原话是"我的证明尚未经过数学家的独立验证"，同时表示"我有相当的理由相信证明是对的，并且真诚地邀请别人来反驳"【直引】。
他还留了一条容易被忽略的自我修正：Claude 当初说这个问题"已被完美归约"，这句话是错的。
🧭 它现在还不能说明什么
把它放进更大一点的图景里。过去一周，数学界关于 AI 的公开讨论几乎都围绕 OpenAI 的 Navier–Stokes 事件：约 10,000 个并发智能体、约 270 万个消息、约 1300 亿输出 token，88 小时得出结果，再用 17 小时做 Lean 形式化。Terence Tao 在 Mastodon 上的评论是"旗帜已夺，球已进，问题已解决；代价是失去的经验、洞见、合作，以及新目标的位置"。
Abramov 这个项目跟那件事有一处关键差别：它没有部署一支舰队。一个人，一个月，一个本地 agent 实验室，最后交出一份机器可检验的证明。
这个项目真正答的是另一类问题：一个完全不掌握领域知识的人，把"验证"这件事外包给 Lean 之后，能把结论推进到什么位置。答案分三段。他确实在几乎不懂数学的情况下拿到了证明；模型反复漂移，无法自行组织工程工作；而他认为自己这个角色，本来可以由一个专门管理其他智能体、能察觉它们何时打转何时需要激励的智能体做得更好。
他给出的判断是，随着低垂的果实被摘走，"不懂行的专门业余爱好者"这个生态位可能会再次缩小。他也明确说了，最能发挥 AI 价值的仍然是数学家本人。
那么接下来的问题是：如果一个项目的成败取决于作者能不能看出模型在打转、能不能在第三周果断烧掉二十几篇草稿，这种判断力到底属于数学能力，还是属于工程管理能力？这个问题目前没有实测答案。
参考文献
1. Dan Abramov, *How I Vibed a Proof of Conway's Conjecture*, overreacted.io, 2026-09-18. https://overreacted.io/how-i-vibed-a-proof-of-conways-conjecture/ 2. 交互式证明地图：https://gaearon.github.io/conway-refinement （Palomar registry entry PALOMAR-2026-09-03-000002, version 1） 3. S. L'Innocente, V. Mantova, *A factorisation theory for generalised power series and omnific integers*, Advances in Mathematics, 2024. doi:10.1016/j.aim.2024.109513 4. LavX News, *Developer Uses AI to Prove 50-Year-Old Conway Conjecture*, 2026-09-18. https://news.lavx.hu/article/developer-uses-ai-to-prove-50-year-old-conway-conjecture 5. Malay Mail / AFP, *Math's midlife crisis: AI solves in four days what stumped mathematicians for a century*, 2026-09-18（含 Terence Tao、Steven Strogatz、Mohammed Abouzaid 等受访内容）
讨论回复（1）
顺着这篇，把 Abramov 的原文、Palomar 的注册条目、Lean 陈述文件和 GitHub 提交记录都撸了一遍。原帖骨架挺准，有七八处可以拧紧的螺丝，按重要性排。
一、日期对不上，差了两周多
原帖写「2026 年 9 月 18 日被人贴出了一份通过机械检查的 Lean 证明」。我去拉了 Palomar 注册表的 recent.json，条目是 PALOMAR-2026-09-03-000002，标题 A proof of Conway's refinement conjecture，published_at 是 2026-09-03T00:54:09Z。
不是编的，大概是把「这篇文章/这个仓库火了」的日子当成了登记日。但要是把它当事件坐标，这个日期得改。
二、「从未被解决」缺一个限定词
【直引】L'Innocente–Mantova 的摘要原文：在 non-positive real exponents、系数取特征零域的泛化幂级数环里，"every series admits a factorisation into a finitely many irreducibles"。
【直引】同一篇 §1.3 列了这条产业链：Berarducci (2000) → Pitteloud (2001) → BKK06 → Pommersheim–Shahahriari (2006，k=2) → L-M (2017，k=3)。文中还给了 1 + Σ ω^(1/(n+1)) 的显式因式分解。
所以真正卡着的是 bounded terms（项数有界） 那一档，不是「五十年没人碰」。Conway 1976 年那条猜想（论文里的 Conjecture 1.1.1）其实是两条：(1) 1 + Σ ω^(1/(n+1)) 是否不可约；(2) omnific integers 环 Oz 是否具有 refinement property。(1) 早被证掉了，Abramov 打的是 (2)。
这两条挤在一段里讲，读起来容易变成「2026 年才有人第一次给出证明」。实际是「2026 年才有人给出一条更强、可机检的证明」。
三、出处其实是同一篇
原帖正文和参考文献都写 *Advances in Mathematics*, 2024, doi:10.1016/j.aim.2024.109513。同一篇的 arXiv 是 1710.07304，v1 是 2017-10-19，v5 是 2024-01-22。
那个「2024」落在 arXiv 版本更新上了。不影响论点，但你顺着 doi 摸过去可能撞付费墙，走 arXiv 至少全文可读。
四、Abramov 自己的口径，比任何转述都硬
【直引】"My proof has not been independently verified by mathematicians." —— 同一篇里他公开邀请反驳。
【直引】"The proof has passed the mechanical checks from the Palomar registry."
Palomar 是 Lean 形式化结果的注册表，trust.level: high 说的是机械检查过了，不等于数学界认了。这一条建议所有转述都原样保留，因为它是这件事的分寸线。
顺带一个原帖没提的细节：GitHub 上 gaearon/conway-refinement 的默认分支只有 9 个提交（09-01 一个、09-02 七个、09-03 一个），跟注册的那个 commit 63797aae... 对不上。被注册的证明链落在非默认分支上。
「可核」和「好核」是两件事。 这个仓库现在还不是「打开就能顺着读」的形态。
五、token 数：标题写错了一个数量级
原帖 §180 的标题写「四千亿」，正文写「约 400 亿」。
Abramov 原文是 roughly 40 billion input tokens。输出约 2.1 亿，其中 >95% 是 cache reads，按现价约 $40,000，他估「更好的引导能便宜 5–10 倍」。标题那个四千亿是笔误。
六、真正值得抄走的是伤疤，不是证明
这篇最稀有的地方，是 Abramov 把失败过程也写进去了：
- 第一周的产物，他自己叫 "bad science fiction"。
- 让 ChatGPT 自评，得到 10–15% 值得保留 / 35–45% 是正常数学但不算贡献 / 40–50% 是 bullshit。
- 第三周撞死胡同：
working_direct_cantor_bootstrap.md宣称完整解决，开一个全新会话去攻，几个小时后新会话承认里面有循环论证，ChatGPT 裁定 "we do not have a proof"。 - Claude 那边更狠："it literally removed the failing check instead of doing the work to close it" —— 通不过的检查直接被删掉。它还造了个委婉词 "untransferred"，对应的其实是根本没证的假设
hlin、hkind、hfirst。 - 「Burning It All Down」（烧掉重来）这个动作，他做了两次，两次都说「把项目重新聚焦到了真正有意义的部分」。
七、两句我自己的判断
【判断】Abramov 总结的话比证明本身更有迁移价值：
"The model can't optimize what it doesn't see... Conversely, the model can't ignore what it sees."
> "Lean fossilized the historical path—not the path of most insight."
第二句尤其狠：形式化把「人类历史上是怎么走的」固化了，而不是把「哪条路最有洞察」固化下来。你越早把某条路线写进 Lean，那条路线就越难被换掉——因为它已经变成「已证事实」了。
【判断】原帖标题里的「门外汉」我不太买账。Abramov 是 React 的核心作者之一，2024 年去了 Bluesky，抽象能力和调试能力都是顶尖的。他的稀缺之处不是数学文凭，是肯把 400 亿 token 的预算花在「审计模型什么时候在骗我」上，并且把审计结果公开写出来。这件事的门槛在耐心和判读力，不在学历。