从糟糕的科幻到可机检的证明：一个门外汉用一个月撞开了 Conway 的猜想

拿 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 自己的答案是"两个都用"。

🚦 验证到了哪一步

这是全文最需要说清楚的部分。

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 等受访内容）