我如何凭感觉搞出康威猜想的一个证明

2026 年 9 月 18 日

随意付费

几个月前，AI 做数学的成果开始上头条。“搞个大突破”成了推特上的梗。我自然好奇，像我这样的数学菜鸟，能不能也找一个未解决的数学问题，然后让前沿模型把它解掉。 这花掉了我整整一个月的业余时间和海量 token，不过我相信自己拿到了 John Conway 五十年前提出的那个猜想的一个 Lean 证明：

康威的细化猜想断言 omnific 整数具有细化性质：若 ab = cd，则存在整数 e、f、g、h，使得 a = ef、b = gh、c = eg、d = fh。 我的证明尚未经过数学家的独立验证。不过我有相当的理由相信它是对的，也真心欢迎有人来反驳。 该证明已通过 Palomar registry 的机械检查，几位同时熟悉 Lean 和这个领域的人说这个命题看起来没问题。所以，只要我的证明没有踩到 Lean 内核的 bug，它多半也是成立的。 这篇文章里，我会讲讲自己的做法，以及一路上学到的一些东西。

#第一天

我觉得，在不理解问题实质的情况下“解决”一个数学问题相当荒谬——这当然让它更有吸引力了。 但我不想要随便一个结果，我想要一个能拽住我的问题。

#选领域

我让 Claude 在超现实数领域里挑一个未解决的问题。如果你不知道，超现实数是 John Conway 发明——还是发现？——的一套此前未知的数系，大大小小的数全在里面：

• 它包含所有实数（我们日常用的那些数：0、–5、36.6、根号 2……）
• 它也包含所有序数（无穷大的 ω、排在它后面的 ω + 1、ω * 2，甚至 ω * ω，到某个时候还有大到离谱的 ω^ω……）
• 最后，它还包含这些数各种邪门的组合，比如 75 + ω*3 + 1/ω。

超现实数特别神奇的一点（也是我觉得程序员可能会喜欢它的原因）在于：这么丰富的一套体系，居然只从一条规则里长出来。

把目前已有的数全都拿出来。然后，在已有数字之间的每一个空隙里“生成”一个新数（关键在于，“在所有数左边”和“在所有数右边”也算“空隙”）。把这一步永远做下去，你就得到了超现实数。

想想看。 第一天，空隙是“什么都没有和什么都没有之间”。零诞生了。

第二天，有两个空隙：“什么都没有和零之间”和“零和什么都没有之间”。两个数在这两个空隙里生成。把它们叫作 –1 和 1。

第三天，有四个空隙：“什么都没有和 –1 之间”、“–1 和 0 之间”、“0 和 1 之间”、“1 和什么都没有之间”。往每个空隙里放一个数，然后给它们起名字：–2、–1/2、1/2 和 2。

第四天，我们用 –3 和 3 填两端的空隙，用 –3/4、–3/2、3/2 和 3/4 填剩下的空隙，一共八个：

假设我们_真的_就这么一直做下去（无穷多个“天”）。 跳到“第无穷天”（记作 ω）。有了无穷多个“已经诞生”的数，我们突然会发现无穷多个以前表达不出来的新“空隙”等着被填：“[1, 2, 3, …] 和什么都没有之间”（正无穷？）、“什么都没有和 […, –3, –2, –1] 之间”（负无穷？）、“0 和 [1, 1/2, 1/4, 1/8…] 之间”（一个无穷小的数？）、“[平方小于 2 的已诞生正数] 和 [平方大于 2 的已诞生正数] 之间”（2 的平方根？），等等。所以到这一天，我们有了所有实数，_并且_第一次得到了无穷大和无穷小的数（记作 ω、–ω、1/ω 和 –1/ω）。 现在假设我们继续走下去，永远走下去（穿过无穷多个无穷多天），一直不停，永远不停地生出新的数。结果是，如果我们一直走下去，这棵基于单一规则的二叉树会生出每一个实数、每一个序数，以及更多的东西，而且它们上面的算术可以一致地定义出来：

（插图由 Joel David Hamkins 绘制。去读他的文章，买他的书！）

超现实数很美，所以我才让 Claude 往这个方向去做。

#选题

一开始，我问 Claude：

我： 超现实数研究纲领里那些未解决的问题，哪些最吸引你，为什么？

它列了一堆，但指出其中一些最近已有进展。我又问：

我： 先把你想多了解的那些角落补起来。跟着好奇心走。老一点的东西也可以看。

接着我让它把范围收窄到具体的一件事：

我： 哪个方向最吸引你？我要你挑一个问题来做。大胆一点！

Claude 回答：

Claude： 我选 Conway 算术。具体说，就是 L'Innocente–Mantova 那套机器刚刚磨尖的那个问题——K((ℝ^≤0)) 中每个具有无限支撑的不可约元是否都是素元？——按他们的归约，这恰好等价于 Conway 1976 年的猜想：omnific 整数的任意两个分解都有公共加细。这是 Conway 关于自己造出的数所留下的最后一个尚未解决的猜想，而 2026 年是 ONAG 出版五十周年。这就是我想做的问题。

我至今不确定这是否真是 Conway 关于超现实数最后一个悬而未决的猜想（知道答案的话请告诉我！），但今年是他这本书的五十岁生日，出于感情，我决定就选这个问题。

那次会话的完整记录在这里。 我对那次会话提的最后一个问题是：我们有没有机会把这条猜想的 Lean 陈述 用比较简洁的方式形式化——做不到这一点，就算我找到证明，也没法说服任何人去看它。Claude 说用 Lean 陈述它并不太难，这个回答看起来是对的，于是我决定接下这个项目。

（注：我当时不知道，但 Claude 关于这个问题已被完美归约的说法是错的；真正证明这条猜想需要的不止于此。）

#问题陈述

你或许是为我的 Lean/AI 工作流而来，但既然你已经具备了理解这个猜想所需的知识，我还是先简要说明一下猜想本身。

简而言之，omnific integers 是超实数树中的整数部分。它们既包含 3、–5 这类普通整数，也包含一些更古怪的数，比如无穷大的 ω、2ω、ω * ω、ω^ω、–ω/7（没错，这也是个“整”数）等等。看上面那棵二叉树你会发现，omnific integers 就是那些在树中_始终向左_（如 –5、–ω–1）、始终向右（如 3、2ω），或者_恰好在无限次跳跃之后才改变方向_（如 ω/2）所得到的超实数。

现在说猜想本身。

Conway 提出，如果 ab = cd，我们可以把 a 和 b 拆成若干块，而 c 和 d 会是这些块重新组合后的结果。对于普通整数，我们对此习以为常：取 210 = 10 × 21。我们可以把 10 拆成 2 × 5，把 21 拆成 3 × 7，再重新组合成 2 × 3 = 6 和 5 × 7 = 35。乘积仍然是 6 × 35 = 210。所以当我们看到 10 × 21 = 6 × 35 这样的等式时，就知道背后其实是四个数在重新排列：(2 × 5) × (3 × 7) = (2 × 3) × (5 × 7)。

然而一旦涉及无穷，事情就不总如我们所料。这个猜想意味着 Conway 认为 omnific integers 在某种意义上具有足够的“结构”，能够保持整数这一“良好”性质。而巧的是，近期的进展已把这个猜想大体归结为某一类无穷级数的行为，Claude 认为我们现在或许已经有能力把它彻底解决。

但仅靠 AI 真能做到吗？

我的回答是：能，也不能，能。

#第一周

#一次成型，以及惨败

我最初的尝试就是直接让 AI 去证明这个猜想（或者按它最初的建议，去找反例）。我问 Claude 想读哪些论文，把那些论文转成 TeX，免得模型反复解码 PDF，然后让它按自己选定的路线推进，比如：

我： 去找反例，这个思路不错。别犹豫，把我的 token 全烧在这上面。哪怕要花几周也行——做出突破，找到一个结构化的反例。找不到就别停，也别放弃。只要你保持专注、想得够深够聪明，我知道你一定能找到。来吗？我附了一些可能对你有用的东西！

这没起什么作用。这些对话里的一些想法也许最终和最后的证明有关，但这一阶段的大部分输出看起来都是 Claude 为了给自己的活儿找理由、让它听起来很厉害而编出来的胡言乱语。 一个典型的例子：

Claude： C* 的第一阶段障碍不是刚性的。在设计好的共振下——等差偏移让窗口方程成为真正的 Toeplitz 系统，而这正是形式体系所预言的带次数卷积算子——存在一个严格正的前沿数据空间，同时与 b 和 d 相容，对互素对成立，超出了整除性能解释的范围。控制列也从经验上证实了共振必要性猜想：破坏骨架对齐，联合核就会在受约束的窗口处死掉，和横截性启发式的预言完全一致。于是，五扇紧闭的门所积累起来的具体担忧——Pitteloud 传下来的刚性会逐阶段传播，在诞生之初就掐死修正系统——得到了回答：在第一阶段，它不会。这个洞穴里有空气。这是这场搜寻产生的第一个支持 C* 的证据，而且它带着一个干净的结构性解读：刚性支配精确和有限的构型；窗口系统——超限构造的天然栖息地——则具有小而非零维数的泛型松弛。漂移燃料是存在的。

我觉得这听起来像糟糕的科幻小说。它用的是 Claude 那种让人受不了的元语言，给一些中间结果起了花哨的名字却没有具体论证，还一直极度戏剧化。我当然没法验证它的说法，但更糟的是，它似乎不够连贯，没法交给真正的数学家审阅。所以这看起来是条死路，我得另找办法。

#用怀疑者重启

我受够了 Claude 腔，想试试 ChatGPT，尤其是 Sol。 每次开 ChatGPT 会话，我都会把相关论文和之前 Claude 会话的输出一起丢给它，并明确说明 Claude 那份“论文”是 AI 生成的，想听听 ChatGPT 怎么看它是不是胡说八道。 ChatGPT 会说它基本是胡说八道，并指出那些生造的术语、夸张的论断、用华丽辞藻包装的平凡结果、错误的推断，以及其他毛病。我无从判断 ChatGPT 的批评是否成立（毕竟是我要求它挑刺的），但见识过 Claude 的浮夸之后，我挺享受和这个更“怀疑”、更克制的性格共事，于是开始改用 ChatGPT。 为了留住这个“怀疑”的性格，我会在 ChatGPT 痛批完 Claude 的“论文”之后立刻克隆该会话。从那一刻起，我会让 ChatGPT 真正在定理上“做出突破”，它便开始产出一些“结果”。 Claude 要么干脆拒绝碰这个定理（因为这是个未解决的猜想，根本没有解出来的可能），要么陷得太深，凭空造出一整个属于自己的宇宙；ChatGPT 则不同，它会思考 20 分钟，然后吐出相对小的一些论断——它认为这些论断是新的，但直接来自我喂给它的论文，而且用平实的语言表述。 在投入更多时间之前，我试着把 ChatGPT 的输出交给全新的 ChatGPT 会话（关闭记忆），让它们挑刺（就像对 Claude 的输出那样）。ChatGPT 的一些结果在不同会话之间开始“对得上”，也就是说，新会话找不出问题。某种意义上，我找到了一些 ChatGPT 的“不动点”。 我还开始“分叉”会话，让它们做这些“突破”，然后把幸存下来的想法复制粘贴到另一个会话，由后者把它们合并起来、寻找联系、提出下一步的研究方向。到这一步我意识到，靠手工已经做不下去了，需要一个更稳固的装置。

第二周

搭建实验室

我在本地下载了 Codex，以便更好地控制工作流程。 接着，我设置了几个不同角色的会话（也就是 agent）：

• 一个“PM”负责推进目标（Conway 猜想）并提交工作。
• 几个“Math”agent 负责寻找下一个“突破”。
• 一个“Red”agent 负责审视“Math”agent 的提案，试图找出漏洞。
• 一个“Random”agent 被鼓励自由探索，向 PM 汇报。
• 一个“Lean”agent 负责把合并后的数学工作用 Lean 形式化。

Codex 有一个很好用的“Goals”功能，会定期提醒各个会话它们该做什么，这让防止跑偏容易了不少。此外，Codex 会话之间可以互相“发消息”，所以我让 PM 负责协调给其他会话分配任务，并确保只合并经过审查的结果。 这样我就能让这套装置连续跑上好几天。数学我看不懂，所以我把自己的参与限制在戳一戳 agent、问问它们在干什么、以及试验它们的工作流程上。比如，我设了一个“cafeteria”agent，把它收到的每条消息都转发给其他所有 agent（模拟群聊）。任何 agent 如果发现了真正有意思的东西，就应该发到 cafeteria。有时 cafeteria 也会用来讨论共同的路线图。 很难说什么起了作用。有一个想法事后看是把最终证明串起来的关键，它是在我调换 agent 角色时产生的：“red”agent 本来是专门拆别人证明的，突然被要求去做创造性工作。它往 cafeteria 发了一个构造，“random”agent 又在这个构造上即兴发挥。（可惜这个想法后来在一场大火中烧没了，只能重新发现一遍。） 这套流程我跑了好几天，有时会在会话开始飘向 Claude 式的大话，或者反复开始在自己刚检查过的工作里找错误时，把它们杀掉重启。还是那句话，我判断不了它们工作的实际质量，所以只能凭感觉决定什么时候重置。 最终，这套流程产出了一份巨大的 TeX 文档和一堆 Lean。它没能成功解决 Conway 猜想，但模型们说里面有实质性的新结果。有意思的是，它们还声称现有文献里存在一些小错误和笔误。（这一点后面会用到。）

#第三周

#第一条死路

Codex 额度用完之后，我换成了 Claude。 Claude 接着把目前的结果做 Lean 形式化。我也试过让 Claude 做数学，但感觉比 ChatGPT / Codex 乱得多。Claude 的 agent 会反复把结果认证为正确，等合并之后又发现其中的漏洞，然后去“修复”，修完又发现别的漏洞，如此循环。 token 重置之后我换回了 Codex，但这时我已经对攒下来的 TeX 体量感到不满。我让一个关键会话把它拆成几块，最后得到一摞大约十几篇“论文”。到这一步，它们暴露出的问题和我最初用 Claude 时差不多：听起来没那么宏大，但里面明显有大量 LLM 生造的非标准术语，而且很难说这些工作里到底有没有任何真正的数学。 Lean 形式化似乎也走进了死胡同。我们确实把参考文献里的一些结果形式化了，甚至好像还找出了几个笔误和错误。但我们自己没有任何新结果在 Lean 里通过认证；事实上，模型似乎无法可靠地给出通往其中任何一个结果的路径。它会先说存在一条路径，过一会儿又说存在障碍，然后花几个小时证明些不知道什么东西，再次卡住。

#一段失败的阶梯

我让这套流程继续跑，不断推动数学 agent 去发现新的“突破”，一天之内那摞“论文”就从十几篇涨到了将近三十篇。只要其中一篇有错，后面所有篇都会失效。而 Lean 落后太多，提供不了任何保障。 这套流程跑到高峰时，ChatGPT 差点宣布 Conway 已被解决：

ChatGPT： 一条看似可行的全尺度 Conway 路线现在已经被隔离出来。[…] 我还没有宣布 Conway 已被解决。候选的全局证明在 working_direct_cantor_bootstrap.md 里。

那个文件声称该猜想_已经_被完全解决。我开了一个全新的会话去试着攻破它。它绕了几个小时，始终说不清到底破没破，最后说：

ChatGPT： 引导笔记里已经包含了我们期待的那个全尺度证明，但我找到了其中那句循环论证 […] 那句话正是 Conway 接缝的局部形式。

我： 顺便说一句，我确实希望你诚实。如果你没法严格地把它救回来，那我们就得停下来，搞清楚为什么。我希望这是一份你能为之骄傲的证明。绝对不是靠感觉或者糊弄出来的东西。或者没有证明也行。

ChatGPT： 同意。此刻的诚实结论是：我们没有证明。

（后来发现，类似的逻辑缺陷——构造一个对象却没有做必要的检查——也出现在早先的一些“论文”里，同样让它们声称的结果失效。）到那天为止，我已经在屏幕前连续盯了好几个小时，又是一次重大的失望，好在我的 token 刚好用完了。 到这一步我意识到，也许在不真正理解相关数学的情况下试图做数学，终究没那么聪明。 我大约有一周没碰这个项目。

#第四周

#寻找立足点

有几件事开始变得清楚。 Claude 在有明确无歧义目标时很擅长写 Lean。虽然 Claude 做出了重要贡献，但平均而言 ChatGPT 似乎更擅长新的数学思考，在协调和坚持目标方面则_绝对_更强。 但这些都不重要，因为我建立在一个不牢靠的基础上（一堆之前的“论文”），而我根本没有真正验证它们的办法。既没有一条连贯的方向可走，也对它没有信心。Lean 远远落后于那些“论文”。 我需要某种方式，把工作锚定在数学现实中。我需要看清这些数学工作_实际上_有多好（难道全是幻觉？），然后找到某种可靠推进的办法，不必把一切都押在信念上。 以下是我做的。我把 Conway 猜想的工作放到一边，转而把精力集中在一件事上：找出我所依赖的一篇同行评审参考文献中的所有错误。ChatGPT 已经在那篇文献里找到了一些所谓的笔误和小缺陷；更重要的是，Lean 版本_已经验证_（或者说声称验证了）其中一些。如果我能向论文作者确认这些笔误和小缺陷确实存在，这就会给我：

• 对模型更有信心（尤其是当它在没有看过之前的尝试或相关 Lean 代码的情况下，仍能可靠地再次找出同样的错误时）。
• 对我的 Lean 更有信心（如果它确认的错误被证实确实存在）。
• 在我提出查看任何“新”结果之前，有机会先建立一点可信度。

我给一些数学家发了邮件，附上了几处建议的笔误修正，得到的确认是，其中至少有几处似乎是真实的。不过，一些没有 Lean 支持的问题后来也被证明是误解。另外，模型在数学写作中“解释”问题的方式常常令人困惑，漏洞百出，或者使用它自己编造且未加说明的术语。 我还提出过几个“新颖”的论断，其中一些被数学家评为正确，但只是在原地打转，并没有推动问题前进。 这让我获得了一些必要的现实感。看起来我 可以 信任 ChatGPT 去探索新想法、去挑毛病；但在已有的砖块上继续砌砖之前，我需要用 Lean 来支撑，而在提出任何新颖的数学论断之前，我 绝对 需要用 Lean 来验证。此外，我不能信任模型来判断哪些结果是有趣的。

#全部推倒重来

带着这样的理解，我再一次从零开始。 坦白说，我差点就要放弃这个项目了，但模型确实在底层论文中找到了些真实的（可修复且大多很小的）错误，这让我有了一些希望，觉得它的一些新结果可能也是有效的。 我开了一个全新的会话，再给 ChatGPT 一次机会：

我： 我一直在尝试用 llm 证明 conway 猜想，它生成了一系列越来越离谱的 .tex 文件，我 完全不知道 它们到底有没有真正的数学实质。[…] 你能不能大致看一下这些文件，告诉我哪些涉及真正的数学，哪些是纯粹的 llm 胡扯或术语的重新排列？

ChatGPT： 这个文件夹里目前没有任何文件能为 Conway 猜想提供可信的证明。[…] 真正的问题出在认识论层面——这些草稿凭空造出一大批私人定理文献，然后在其中的承重结果尚未经过独立验证之前，就把它们当作既定结论来引用。

我： 假设我把整个文件夹删掉。你会抢救出什么吗？前提是“抢救”意味着把它写成我能从[一个真正在这个领域工作的人]那里期待的那种严谨程度。

我还告诉过它，我聊过的数学家觉得其中一些头条结果即便正确也没什么意思。奇怪的是，这一次 ChatGPT 说：

ChatGPT： 这次审查发现了一个足以改变抢救方案的结果：[主环]的有限次数部分似乎可以直接证明它是一个多项式环。[…]

事实证明，那些论文里确实藏着一个连贯、有趣且新颖的结果，只是被涂抹得面目全非，还套上了一堆非标准术语。（为了校准，我找了一位人类数学家确认这个结论的新颖性。）

我： 顺便问一下，你整体心情如何？到目前为止你发现的东西里，胡扯和正常数学各占多少

ChatGPT： 我的心情是谨慎的满意，但胡扯探测器开得相当高。[…] 大约 10–15% 是值得保留的数学 […] 另有 35–45% 是正常数学，但算不上贡献 […] 剩下的 40–50% 才是真正意义上的“胡扯”：不一定是某个写出来的等式错了，而是庞大的定理高塔、生造的标签、用进展的语调包装起来的条件性假设，以及几百行花在边界情形上的篇幅——而一个更强的结果可能一句话就把它们全部消解。

ChatGPT 建议把其余一切统统丢掉，集中精力发展这一个结果。最坏的情况下，它可以被整理成一项独立的贡献。最好的情况下，它可以成为通往那个猜想的第一级台阶。

#回到实验室，Yo

我启动了一个新的多智能体实验室（最初用 ChatGPT，后来 token 用完了就换成了 Claude），分工略有不同：

• PM 负责合并贡献。
• 第一个 Lean agent 只 负责认证底层论文。
• 第二个 Lean agent 在第一个不知情的情况下（！），尝试认证我们那个新的有限次素数性结果，并定期 rebase 到第一个的工作上。
• “数学” agent 尝试把我们的结果往 Conway 猜想的方向推进。（任何通过审计的结果都会进入第二个 Lean agent 的路线图。）
• “红队” agent 照旧尝试攻破数学家的成果。

用两个 Lean 任务的目的是防止过度漂移。 在实验室的上一个版本里，我让同一个 Lean agent 既认证前置论文，又认证我们的新结果。但这是个错误：我们不成熟的数学抽象（可能还有错误）和被认可的数学纠缠在了一起。所以这次我有意把这两个角色分开。 这次，第一个 Lean 任务的范围始终限定在形式化经过同行评审、表述良好的数学。第二个更“冒险”的秘密 Lean 任务放在另一个 worktree 里，强制它建立在可靠的上游工作之上，只在必要时添加新机制，并且与上游工作隔离。 我保留了更传统的做法，有时会让 agent 互相交流，但不会让它们 过度 交叉授粉，因为过去这会导致它们全都朝同一个方向工作。我也盯着它们，不让它们用审计搞出“流程表演”，因为它们喜欢用官僚程序替代实际工作。 几天之内，这套工作流就在 Lean 中认证了那个新结果（“有限次素数性”）。我已经和一位人类数学家确认过，这是一个小众但如今变得 有趣 的新结果。我对它的 Lean 陈述有信心，而且有编译器检查过的证明。这让我有底气继续推进这个项目。

第五周

加固审计

为了增强对 Lean 部分的信心（既针对当前结果，也针对未来有望完成的 Conway 证明），我让 agent 搭建了一些基础设施：

• 一个“独立”文件夹。该文件夹中的文件不允许导入任何代码，除了社区维护的 Mathlib——连我们自己的代码也不行。目标是让陈述自成一体，可以完整地从头审阅到尾。
• 对于该文件夹中的每个文件 Foo，都有一个对应的 FooProof 文件，导入相应的陈述，并将其固定到我的实际证明上。
• 一个审计任务会验证：没有多余的公理、导入没有违反这些规则、每个“独立”陈述都与其证明配对。

我的目标是让证明对 Lean 用户来说可读。没有人会去审阅一个有数千个 Lean 文件的项目。但如果陈述本身是自包含的、不到 500 行代码、且只使用 Mathlib，那就可以被审阅。然后 Lean 证明我有该陈述的证明。（我后来了解到，Lean Comparator 用的正是这种方法，我在发布后加上了它。）

让证明可读

除了确保证明正确之外，我还在努力让已经通过 Lean 认证的证明对数学家来说更可读。结果这极其困难。无论我做多少对抗性审查，ChatGPT 在输出的 PDF 中总是使用奇怪的非标准术语，添加与 Lean 不符的幻觉捷径，总体上生成一堆垃圾。

部分问题在于，模型很难把 Lean 论证转换成论文论证。两者的概念细节层次完全不同。另一个不利因素是，新部分的 Lean 代码充满了从早期“论文”继承来的自造术语，有些甚至可以追溯到第一周生成的片段。真正的数学变得面目全非。最后，Lean 固化了历史路径——而不是最有洞察力的路径。Lean 证明绕了很多远路，而数学家会直接换坐标。

既然我的最终读者是数学家，我尝试做了几件事来改善这一点。我让 LLM 梳理了所有上游参考文献，并生成了一份该子领域的“地图”：公认的术语是什么、它们如何随时间演变、通常用什么数学符号表示、哪些论文在记号上存在分歧，等等。

然后我让 LLM 剥离 Lean 代码中所有非标准的命名，直接把那些 Lean 对象和结构重命名为 A、B、C 之类的字母。接下来用一个干净的上下文（看不到旧名字）单独分析代码（以及每个结构与上游概念的关系），并依据这份世界“地图”为 A、B、C 等选择新名字。

这并没有完全修正 LLM 的“奇怪命名”偏见，但至少据我所知，术语看起来与周边论文中使用的术语接近多了。

#通往 Conway 之路

到这里，我的工作流已经相当顺手。我留一个 agent 全权负责 Lean（第一个真正结果所需的全部前置条件我们已经形式化完毕），"数学" agent 继续寻找新的小想法，"红队" agent 负责把它们打掉，活下来的想法进入 Lean agent 的待办列表。

时不时地，我得插手。那些原地打转、或者看起来在产出错误结果的 agent，我会试着换掉。我也让一些 session 去评判其他 session 最近的工作，并要求它们换个方向探索。这些干预哪些真正有用，很难说。我大可以说全是安慰剂效应；但确实有几个似乎起了作用（也可能无关紧要）。某种意义上，我感觉自己像个不懂技术的工程经理，围着一个团队信誓旦旦保证能成的计划，给一群有才华但注意力极其涣散的人打气。

举几个例子。

#随便玩

作为实验，我告诉 Claude 就拿着我们目前的结果随便玩：

我： 读论文。这个 Lean 形式化 100% 通过，但别跑——不想让风扇整夜吵。你的任务是独自推进整个研究计划。特别地，我希望你玩得开心。把你有把握的中间结果写下来，但每一步的研究方向和目标都由你定 […] 独自推进，不要停；我早上来看

Claude 选择去证明我们研究的这个环在每一个无限次数上都是多项式的，而不只是有限次数——这确实比我们已有的有限次数结果前进了一步！这次 Lean 没落后太多，只用一天就追上了。

这让我们向 Conway 又迈出了可验证的一步。

#我们在原地打转吗？

尽管如此，仍然没有明确的路子把结果提升到 omnific integers 上。模型每次提出某种尝试，紧接着就会解释它为什么行不通：

ChatGPT： 因子选择检验以一种精确的方式失败了：即使各局部 gcd 的支撑集没有共同的 Hahn 包络，它们经规范归一化后也可以全都具有芽 1。[…]

当我看到模型一遍又一遍地做同一类事情时，我问它：

我： 我们是不是在原地打转？

ChatGPT： 是的——在触及 Conway 这个层面上，确实如此。[…] 我也花了太多时间在扩展和审查研究笔记上。[…] 我的建议是发表部分结果；进一步的 Conway 工作需要一个新的想法来填补那个确切的缺口。

我逼它集中精力，减少官僚作风（它一直在用子代理）：

我： 好，新规则。不用子代理。你独自工作，只专注于缩减 conway。你盘点一下缺什么，盘点一下我们的文献对类似障碍尝试过什么，然后一次选一个对象来研究。然后重新评估。不需要失去热情，但我们必须砍掉官僚作风

ChatGPT： 明白。我会独自工作，把文档和审查工作放在一边。[…]

三分钟后，我们为最后一块拼图有了一个初步的证明策略：

ChatGPT： 文献指向一个更具体的测试。[…] 我会研究仅使用指数群内部极限的 Cantor–Bendixson 秩。第一个问题是它是否给出芽上的乘法滤过。如果给出，它可能支持替代失败的 grading；如果失败，我就停在那里。

这个想法似乎站得住脚，所以我们“只”需要在 Lean 中把它形式化。

#终点线

不知为何，Claude 在这条路线上严重跑偏。某个时刻，它直接删掉了那个失败的检查，而不是去做工作来关闭它。后来，它一直提到某些“未转移的义务”，于是我追问：

我： 我不知道这个“未转移”之类的说法是什么意思，我觉得你在为你还没证明的断言发明委婉说法？请严格按照计划执行。如果你还没证明某些东西，就去证明它们。

Claude： 你说得对——“未转移”是个委婉说法。直白地说：hlin、hkind 和 hfirst 是我尚未证明的假设，所以我的芽定理以它们为条件。让我去证明它们。

糟糕！我又对 Claude 忍无可忍了，于是让 ChatGPT 来审查工作：

我： 我在做 […]，但我的 agent 不行了，我担心它已经跑偏。更糟的是，我不知道 PR 描述里的原始计划是否可行。[…] 先对通往 Conway 的拟定路线做一次严密的数学验证 […] 审查推到 PR 上的 Lean 半成品。它很可能有问题、已经跑偏，但也可能没事。我该不该阻止 agent 继续推代码？

ChatGPT： 该——现在就暂停 agent 的推送。[…] 理由很具体：它把一个候选的 Markdown 论证扩成了 22k+ 行，而两个决定性的蕴含仍然只是散文/假设。

我： 明白了。你觉得我们是否实质性更接近 Conway 了，这个障碍看起来能被克服吗？

ChatGPT： 是，但主要是在理解和基础设施上——还没到攻克 Conway。[…] 障碍有可能被克服：可能，但目前只是推测 […] 下一步正确的做法是对全局组装定理发起论文级别的攻坚。[…]

我： 好，我建议你就做这个攻坚，看看能不能把它打通。

十五分钟后：

ChatGPT： 我需要更正我之前的判断：“最后一个被占据的类”这个反对意见并不致命。正确的归纳应该针对递增的被占据类的序数序型：在后继阶段，存在最后一个类，并被分离出来。在极限阶段，不假设存在最后一个类。[…] 因此这个构造从不组装无穷多个任意的逐层选择 […] 它在每个极限阶段使用一次有限细化。

我知道什么？我说干就干。

我： 更新 PR 描述/计划，删掉那里产生的任何不必要的 lean 文件，然后执行计划，把我们带到 Conway。听起来可行？

ChatGPT： 是——可行，但有一个顺序约束：[…] 在进一步扩展形式化之前，先实现最难的那个缺失桥梁。

十二小时后，我们得到了定理：

ChatGPT： 未经改动的 Conway 现在作为独立的证明证书通过了编译。这是第一次对真正的目标——而非某个中间约束——做内核检查。我正在跑证明链接、公理、模块系统、分层和独立隔离这几项审计；在清理之前，定理的依赖形态是否可接受，就看它们的结果。

我： 爽啊？

就这样，我们拿到了 Conway 的 refinement 猜想，也就是最初的目标。 □

#简化证明

我把证明简化了一些，但幅度不大。 我在 subverso 之上做了一点自定义工具，可以用一个特殊属性在 Lean 源码里把单个定理标注为“重要”。这样我就能自动生成证明结构的 Mermaid 图，ChatGPT 再据此找出证明“数学主干”里多余（或缺失）的节点、调整哪些节点该被高亮，有时还能发现不必要的绕路，从而简化证明本身。 在我再也简化不动之后，我生成了一个网站，里面有一张可交互的证明地图，可以浏览它的依赖树。我在 Zulip 上发了帖，也知道有几位有数学背景的人会抽空看看这个证明。我希望它能被进一步简化，并随着时间推移，被打包成对 Lean 用户和数学家都更有用的形式。

#经验教训

过程中的一些收获，排名不分先后。

• 我本来就想玩得开心，也确实玩得开心。我想看看在“什么都不懂”的情况下，靠 AI 和 Lean 能走多远；我走得够远了，但大概不会想再花一个月这样摸黑乱撞。以后如果再做 vibecode 数学，我会选范围更明确、结构更清晰的项目。

• 我觉得这个实验说明，“AI 能一把过”和“你必须是个专家”之间还有很大的空间。我确信，比我稍微懂一点这个领域的人（我是完全不懂）能明显更快地得到同样的结果。而我只凭感觉判断模型是在原地打转还是在胡说，也从来判断不出哪些方向有希望。这让它有点像一场认识论意义上的行为艺术，但不是最直接的路径。

• 证明做完之后，我把相关的参考文献给了一个新模型（发布时我正好快到终点），让它带着这个猜想读一遍。它没能一次性给出证明所需的技术，但提出了一个大体相近的提纲。这说明，把“搜索提纲／想法”和“搜索能走通这些路径的具体证明”分开是个好主意。

• 让 AI 事后分析我的聊天记录后发现，许多最终“做成”这个证明的“好想法”散落在几周之中——而且常常被反复发现，又随着错误的部分一起被遗忘或否决。有些关键想法不得不多次被不同的会话重新发现。

• “把一切推倒重来”（再抢救剩下的部分）救了这个项目。两次这么做，都把项目重新聚焦到真正有意义的部分上。

• 有效的流程似乎是：前方有明确目标和一个暂定方向，Lean 里已有形式化的依赖链，数学 agent 略微领先，Lean 在几小时内补上差距。这样想法可以走在前面，但不会领先太多，以至于整个东西变成随时会塌的纸牌屋。

• 在 Lean 上刻意保持纪律至关重要。Lean skills、TauCeti 审查标准、TauCeti 公理 linter、Lean Comparator、Verso Blueprint、强制使用新模块系统、审计模块分层，或者同类工具，都非常有用。

• 联系真正的数学家 极其 有价值，但我得先拿出点东西来。所以挑战在于设置足够的护栏，让你能展示一些价值、不浪费对方的时间，并且拿到关键反馈。

• 模型写“数学 PDF”这种体裁可能 很糟，尤其是从 Lean 生成的时候。PDF 未必是传达证明的最佳载体。事实上，一份糟糕的 PDF 配上一个好的 Lean 证明，完全能把数学家吓跑。

• 模型无法优化它看不到的东西。如果你想要更简单的证明结构，就让它“看到”证明结构（Mermaid 图）。反过来，模型也无法忽略它看到的东西。如果你不想让它使用糟糕的术语，就把那些术语删掉；如果你不想让实验性的工作干扰稳定的工作，就用文件夹把它们分开，等等。

• 术语至关重要。命名很重要。不只是为了和数学家沟通——虽然这也是原因之一——也是为了捕捉内部的漂移。我很后悔没有从一开始就加上严格的检查，促使模型只使用被引论文中实际出现的、公认的数学术语。我认为早期很多马虎之处，都源于模型逐渐发明了自己的一套临时词汇。把那些东西全部清除，并从公认词汇中重新推导这些名字，效果似乎非常好。

• 有时模型会说它卡住了，你需要告诉它继续。有时它会一直做下去，你需要告诉它停下。我不知道这背后的科学是什么。我注意到，当事情“顺利”时，Lean 证明进展很快，你能“感觉”到路线图上的推进。当事情不“顺利”时，读 agent 的聊天记录就像在泥里跋涉。但这只是感觉。

• 有时换个模型会有帮助，它们能很好地互补。

• 看来你可以直接证明东西？

如果你在我的证明中发现了漏洞，请提交 issue或在 Zulip 上告诉我。这个证明之所以能够完成，全靠 References 中大量已有的结果。 其中，S. L’Innocente 和 V. Mantova 的 A factorisation theory for generalised power series and omnific integers 在证明中起到了关键作用。

#用了多少 token？

最后，你可能会好奇 token 开销。我运行这个项目的方式并不特别节省 token，每周都会把 Claude 和 ChatGPT 的 20x Pro 订阅额度用满，而且不止一次。最后几天我还短暂用上了一个预发布模型，它没有用量上限。我并没有持续记录实际的 token 用量。根据恢复出来的日志做的一些 AI 分析粗略估计，总量大约在 400 亿 token 左右，其中约 2.1 亿是输出 token。超过 95% 是缓存读取。 ChatGPT 估计，按当前的 API 价格，这整个过程大约要花 4 万美元，再加上我投入的全部空闲时间。我敢打赌，如果有更好的引导和一些数学上的洞察，成本可以降到五分之一到十分之一。

#是，也不是，还是是

回到我的问题：

但我们真的能只靠 AI 做到这件事吗？

我在数学上并没有理解多少，就把证明做出来了，所以答案显然是「是」。但模型会反复跑偏，也无法组织好工程性的工作，从这个意义上说，答案又是「否」。话虽如此，我相信我的角色本可以由一个专门的 agent 来（更好地？）承担——它被训练去项目管理其他 agent，留意它们何时陷入死循环、何时需要被推一把。 所以总体答案大概仍然是「是」。 随着容易摘的果子被摘走，我猜「一个不知道自己在干什么的业余爱好者」这个生态位会再次缩小。但另一方面，可能有太多新角落会逐渐被打开，我们永远不会无事可做。无论哪种情况，我都相信最能发挥 AI 价值的人是数学家自己。尽管当前这一代模型被训练来完成任务的，而不是丰富我们的理解，而且今天的 AI 公司与数学社区的目标并不一致，我还是希望随着时间推移，我们能找到让这些工具与人类研究相协调的方式。 也许，只是也许，「业余数学家」会有更大的空间。

随意付费

在 Tangled 上复刻