我是如何借助 AI 与 Lean 证明康威50年猜想的：Dan Abramov 的一月通关实录

How I Vibed a Proof of Conway’s Conjecture

文章背景与核心概要

本文记录了著名技术开发者 Dan Abramov 作为一名自称的“数学小白”，如何仅凭前沿大语言模型 (Claude 与 ChatGPT) 以及交互式定理证明工具 Lean 4，历时一个月攻克传奇数学家 John Conway 悬置整整 50 年的“全数整数细分猜想” (Omnific Integer Refinement Conjecture) 的奇幻实录。在经历初期 AI 严重胡言乱语、“黑话”满天飞与伪证明破产的泥潭后，作者开创性地搭建了包含项目经理、红队攻防、文献逆向与形式化编译的多智能体协同实验室架构。通过严格的代码隔离、定理反演与编译器内核硬校验，最终成功编译出了一份经 Lean 4 内核无额外公理检验通过的完整证明证书。本文兼具幽默坦诚的个人叙事与前沿形式化验证的深度思考，展现了生成式 AI 赋能前沿跨界探索的巨大潜能。

核心概要

Summary

一名自称“数学小白”的业余爱好者，耗时整整一个月，完全凭借前沿大语言模型 (Large Language Model, LLM) —— Claude 与 ChatGPT，以及形式化定理证明工具 Lean 4，向数学界的公开未解难题发起了冲击：试图证明 John Conway 在 50 年前提出、关于超现实数 (Surreal Numbers) 的全数整数细分猜想 (Omnific Integer Refinement Conjecture)。尽管起初遭遇了严重的 AI 幻觉（充斥着大量虚构行话的“AI 垃圾内容”），作者随后精心打造了一套多智能体协同实验室工作流，结合严格的 Lean 4 形式化验证、独立代码文件沙箱隔离与层层递进的红队审计机制。最终，整套系统成功编译出了一份经 Lean 4 编译器内核完备校验的康威猜想证明证书，并向全球数学界同行公开邀请形式化证伪。

An amateur mathematician ("math noob") spends a month using AI frontier models (Claude and ChatGPT) and the Lean theorem prover to attempt an open mathematical problem: proving John Conway’s 50-year-old omnific integer refinement conjecture regarding surreal numbers. Despite initial struggles with AI hallucinations ("slop" and made-up terminology), the author builds a multi-agent laboratory workflow combined with rigorous Lean formalization, independent file isolation, and step-by-step audits. Ultimately, the system successfully compiles a kernel-checked proof certificate of Conway's conjecture in Lean, inviting formal peer refutation.

我是如何“凭直觉与感觉”搞定康威猜想证明的

How I Vibed a Proof of Conway’s Conjecture

日期： 2026年9月18日
作者： Dan Abramov (Ko-fi | GitHub 源码仓库)

Date: September 18, 2026
Author: Dan Abramov (Ko-fi | GitHub Source)

几个月前，AI 在数学领域取得突破的新闻开始频频登上各大媒体头条。“搞个大突破” (Do a breakthrough) 甚至成了 Twitter 上的热门技术热梗。自然而然地，我也按捺不住好奇心：像我这样一个连高等微积分题解都要到处找答案的数学小白，是不是也能随便找一个悬而未决的数学开放难题，然后让前沿模型帮我把它解出来？

A few months ago, AI math results started making headlines. “Do a breakthrough” became a Twitter meme. Naturally, I became curious whether I, too, a math noob, could find some open mathematical problem and then have a frontier model solve it.

这花光了我整整一个月的全部业余时间，并烧掉了天文数字般的 Token；但我想，我已经成功拿到了由 Lean 4 严格检验通过的数学证明，攻克了 John Conway 在 50 年前留下的这一著名猜想：

It took me an entire month of my free time and a boatload of tokens, but I believe I’ve obtained a Lean proof of this conjecture posed by John Conway 50 years ago:

Conway 的细分猜想断言：全数整数具备优良的因数细分性质——如果四个全数整数满足 \(ab = cd\)，那么必然存在另外四个整数 \(e, f, g, h\)，使得 \(a = ef\)、\(b = gh\)、\(c = eg\) 且 \(d = fh\)。

Conway’s refinement conjecture claims that omnific integers have a refinement property: if ab = cd, there are integers e, f, g, h with a = ef, b = gh, c = eg, d = fh.

需要坦诚说明的是，我的证明目前尚未经过人类专业数学家的独立同行评审。不过，我掌握着相当扎实的依据相信这一证明是坚实成立的，并且我非常真诚地欢迎任何人前来挑错和证伪。

My proof has not been independently verified by mathematicians. However, I have decent reasons to believe the proof is correct, and I genuinely invite a refutation.

目前，该证明已经完全通过了来自 Palomar 注册表的严格机械化检查，几位精通 Lean 4 和该领域的专家也确认形式化命题本身的陈述完全准确。因此，只要我的证明代码没有意外触发 Lean 4 底层内核的致命 Bug，那么它大概率也是货真价实成立的。

The proof has passed the mechanical checks from the Palomar registry, and a few people familiar with both Lean and the field said that the statement seems correct. So, assuming my proof doesn’t rely on a Lean kernel bug, it’s likely to be legit too.

在这篇长文中，我将详细记录我的探索路径，以及一路上所踩过的坑和收获的认知。

In this post, I’ll describe my approach, and some things I learned along the way.

第一天

First Day

我一直觉得，“在完全不懂数学本质的情况下把它解出来”这个念头既荒谬又离奇，但恰恰是这种荒诞感，让这件事显得格外诱人。

I thought the idea of “solving” a math problem without understanding its substance is rather absurd, which of course made it all the more appealing.

不过，我可不想随随便便找个平庸的题做；我想要的是那种能够真正牵引我、让我心潮澎湃的问题。

However, I didn’t just want any result; I wanted something that pulls me.

确定研究领域

Choosing the Field

我让 Claude 在超现实数 (Surreal Numbers) 的研究版图中挑选一个开放性难题。如果你之前没听说过，超现实数是 John Conway 凭借天才灵感发明——抑或是发现？——的一个全新数系，它将宇宙中所有大大小小的数字统统包罗在内：

I asked Claude to pick an open problem in the field of surreal numbers. In case you’re not aware, surreal numbers are John Conway’s invention—or a discovery?—of a previously unknown number system containing all numbers great and small:

• 它包含了所有的实数 (Real Numbers)（比如我们日常接触的 0、-5、36.6、根号 2……）；
• 它还包含了所有的序数 (Ordinal Numbers)（无限大的 \(\omega\)、紧随其后的 \(\omega + 1\)、\(\omega \times 2\)、乃至于 \(\omega \times \omega\)，甚至是超乎想象的超大基数 \(\omega^\omega\)……）；
• 最后，它还包含了它们之间各种光怪陆离的组合，比如 \(75 + \omega \times 3 + 1/\omega\)。

• It contains all real numbers (the numbers we use like 0, –5, 36.6, square root of 2…)
• It also contains all ordinal numbers (the infinitely large ω, the ω + 1 that comes after it, the ω * 2, and even ω * ω, at some point even the impossibly large ω^ω…)
• Finally, it contains all kinds of unholy combinations of them, like 75 + ω*3 + 1/ω.

超现实数最不可思议的奇迹之处（这也是我觉得程序员会对它欲罢不能的原因）在于：如此博大精深的庞大数系，竟然完全由一条极其优雅单纯的简单法则繁衍而来。

What is particularly miraculous about surreal numbers (and why I suppose they might appeal to a programmer) is that this rich system spawns from a single rule.

💬 [原文法则 / Original Rule]: 取出你目前拥有的所有数。然后在已有数字之间的每一个“空隙”中“孕育”出一个新数（最关键的是，“所有数的左侧”和“所有数的右侧”也算作“空隙”）。永远重复这一步骤，你就会得到超现实数。

Take all the numbers you have so far. Then, “spawn” a new number in every gap between the numbers you already have (crucially, “to the left of all” and “to the right of all” also count as “gaps”). Apply this step forevermore, and you’ll get surreal numbers.

让我们仔细品味一下这个过程：

Think about it.

第一天，世间只有唯一的一个空隙——“在空无与空无之间”。于是，0 诞生了。

On the first day, the gap is “between nothing and nothing”. Zero is born.

第二天，出现了两个空隙：“空无与 0 之间”以及“0 与空无之间”。两个新数在这两个空隙中诞生。我们把它们分别命名为 -1 和 1。

On the second day, there are two gaps: “between nothing and zero” and “between zero and nothing”. Two numbers spawn in those two gaps. Call them –1 and 1.

第三天，衍生出了四个空隙：“空无与 -1 之间”、“-1 与 0 之间”、“0 与 1 之间”以及“1 与空无之间”。在每个空隙里各填入一个数，分别命名为：-2、-1/2、1/2 和 2。

On the third day, there are four gaps: a gap “between nothing and –1”, a gap “between –1 and 0”, a gap “between 0 and 1”, and a gap “between 1 and nothing”. Put a number in each of those gaps and then give them names: –2, –1/2, 1/2, and 2.

第四天，我们在边缘的两个空隙填入 -3 和 3，并在其余各处空隙依次填入 -3/4、-3/2、3/2 和 3/4：

On the fourth day, we fill the eight gaps with –3 and 3 at the edges and –3/4, –3/2, 3/2, and 3/4 in the remaining gaps:

设想一下，如果我们真的将这个过程永远持续下去（经历无限多步），然后再超越无限继续孕育（无限次无穷步），如此生生不息、永不停歇地衍生新数。令人惊叹的是：仅仅基于这一条极简法则构成的二叉树，最终将生长出每一个实数、每一个序数以及更多无法想象的数，并且全部配备自洽完整的四则运算律：

Suppose we actually do this forever (an infinity of steps), then forevermore (an infinity of infinities of steps), and so ever on and on, never stopping birthing new numbers. It turns out that the binary tree based on this single rule will eventually give us every real, every ordinal, and more, with consistent arithmetic on them:

（图解由 Joel David Hamkins 绘制。强烈推荐大家阅读他的博文并购买拜读他的著作！

(Illustration by Joel David Hamkins. Go read his posts and buy his book!)

超现实数的美感令人震撼，正因如此，我当即决定让 Claude 在这个领域寻找突破口。

Surreal numbers are beautiful, and that’s why I asked Claude to work in that area.

选题敲定

Choosing the Problem

最初，我向 Claude 抛出了问题：

Initially, I asked Claude:

💬 [原文对话 / Original Dialogue]: 我： 在超现实数的研究项目中，哪些悬而未决的问题最能吸引你？为什么？

Me: which unsolved problems in the Surreal Numbers research program pull you the most and why?

它列出了一长串备选清单，但也提到其中一些问题近期已经有了突破。我接着指示道：

It suggested a number of things but noted some have had recent progress. I asked:

💬 [原文对话 / Original Dialogue]: 我： 去深入了解一下那些你渴望探索的未知盲区。顺着你的好奇心走，年代久远的经典课题也可以看。

Me: get up to speed on the corners you want to know more about. follow your curiosity. you can look for older stuff too.

随后我进一步要求它将范围缩小到一个具体的标的：

Then I further asked it to narrow down the choice to something concrete:

💬 [原文对话 / Original Dialogue]: 我： 哪个方向最能激起你的斗志？我需要你拍板挑一个具体的问题来攻克。大胆一点！

Me: what direction pulls you most? i want you to pick a problem to work on. be bold!

Claude 回复道：

Claude replied:

💬 [原文对话 / Original Dialogue]: Claude： 我选 Conway 的算术理论。特别是刚刚被 L’Innocente 与 Mantova 的理论体系 彻底聚焦的核心疑问——在具有无限支集的 \(K((\mathbb{R}^{\le 0}))\) 中，每一个不可约元是否都是素元？通过他们的化简，这如今恰好等价于 Conway 在 1976 年提出的著名猜想：任意一个全数整数的两种因子分解，必然允许一个公共的精细细分。这是 Conway 关于他自己发现的数系中，至今唯一悬而未决的最后遗留猜想，而 2026 年恰好是他的巨著 《论数与博弈》 (ONAG) 出版 50 周年纪念。这就是我最想全力攻克的难题。

Claude: I pick Conway’s arithmetic. Specifically, the question the L’Innocente–Mantova machinery just sharpened to a point — is every irreducible in K((ℝ^≤0)) with infinite support prime? — which, by their reduction, is now exactly equivalent to Conway’s 1976 conjecture that any two factorizations of an omnific integer admit a common refinement. It’s the last of Conway’s own conjectures about his own numbers still standing, and 2026 is ONAG’s fiftieth birthday. That’s the problem I’d work on.

坦白说，我至今也不确信这究竟是不是 Conway 关于超现实数留下的最后一个未解猜想（如果有读者知情，欢迎不吝赐教！），但今年恰逢该书出版 50 周年，这份浪漫的情怀促使我决定就选它了。

I still don’t know whether this really was Conway’s last standing conjecture about the surreal numbers (let me know either way!), but this year being his book’s 50th birthday convinced me to choose this problem for sentimental reasons.

这是那一轮对话的完整原始记录。 我在那个会话中的最后一个问题是：我们是否有机会在 Lean 4 中用相对简洁的形式化语法把这个猜想的命题形式 (Statement) 明确定义出来——如果没有这个前提，就算我撞大运摸索出了一份证明，也根本无法说服任何正统数学家多看它一眼。Claude 坚定地表示在 Lean 4 中表达它并不困难，而且听起来言之凿凿，于是我决定正式启动这个项目。

Here is the full transcript from that session. My last question to that session was whether we have a chance of formalizing the Lean statement of the conjecture in a relatively concise way—without that, even if I found a proof, there’d be no way for me to convince somebody to look at it. Claude said it can be stated without much trouble in Lean, and that answer seemed right, so I decided to take on this project.

（注：当时我对此毫不知情，但实际上 Claude 声称该问题已被彻底化简完全是一句谎言；要真正证明该猜想，所需要的远比它说的更加庞杂深奥。）

(Note: I didn’t know this at the time, but Claude’s claim about the problem having been perfectly reduced was wrong; actually proving the conjecture required more than that.)

命题详解

The Problem Statement

虽然大家点进这篇文章主要是想了解我的 Lean 4 与 AI 协作工作流，但我还是想通俗地科普一下这个猜想本身，因为根据前文的介绍，你已经具备了理解它的全部基础知识。

While you’re probably here to learn more about my Lean/AI workflow, I’ll briefly explain the conjecture itself, since you already know enough to understand it.

简而言之，所谓的全数整数 (Omnific Integers)，就是超现实数二叉树中的“整数部分”。因此，它们不仅涵盖了像 3、-5 这样的常规日常整数，还包含了更加奇诡的数字，比如无限大的 \(\omega\)、\(2\omega\)、\(\omega \times \omega\)、\(\omega^\omega\)，甚至是 \(-\omega/7\)（没错，这在超现实数里也是一个不折不扣的“整”数）等等。如果你观察上面的二叉树就会发现，全数整数就是那些你在生成路径上永远向左拐（比如 -5、\(-\omega-1\)）、或者永远向右拐（比如 3、\(2\omega\)）、又或者严格只在跨越无限跳跃之后才改变方向（比如 \(\omega/2\)）而得到的超现实数。

In short, omnific integers are the integer part of the surreal number tree. So they include all regular integers like 3, –5, and so on, but also the weirder numbers like the infinitely large ω, 2ω, ω * ω, ω^ω, –ω/7 (yes, that’s a “whole” number), etc. If you look at the binary tree above, you’ll notice that the omnific integers are the surreal numbers that you get if you only ever go left (e.g. –5, –ω–1), or only ever go right (e.g. 3, 2ω), or only ever change directions exactly after infinite jumps (e.g. ω/2).

现在，我们来看这个猜想。

Now, the conjecture.

Conway 提出：只要满足 \(ab = cd\)，我们就能把 \(a\) 和 \(b\) 拆解为更小的碎片积木，而 \(c\) 和 \(d\) 无非就是同一批碎片积木以另一种方式重组得到的结果。对于我们普通的小学整数乘法，这完全是天经地义的：比如 \(210 = 10 \times 21\)。我们可以把 10 拆解为 \(2 \times 5\)，把 21 拆解为 \(3 \times 7\)；然后重新组合成 \(2 \times 3 = 6\) 以及 \(5 \times 7 = 35\)。两者的乘积依然是 \(6 \times 35 = 210\)。因此，当我们看到 \(10 \times 21 = 6 \times 35\) 这样的等式时，我们心知肚明这背后本质上是四个基本因子在重新排列：\((2 \times 5) \times (3 \times 7) = (2 \times 3) \times (5 \times 7)\)。

Conway suggested that if ab = cd, we can break a and b into pieces, and c and d will turn out to be the same pieces recombined. With regular integers, we take this for granted: take 210 = 10 × 21. We can break 10 down as 2 × 5 and 21 as 3 × 7, then reshuffle them into 2 × 3 = 6 and 5 × 7 = 35. The product is still 6 × 35 = 210. So when we see some equality like 10 × 21 = 6 × 35, we know that under the hood there’s actually four numbers being reshuffled: (2 × 5) × (3 × 7) = (2 × 3) × (5 × 7).

然而，一旦涉足无穷大的深水区，事情往往就会背离我们的常识直觉。因此，该猜想的核心含义在于：Conway 坚信即便到了全数整数的宏大世界中，它们依然拥有某种充沛的“内部代数结构”，足以保全常规整数身上这种优雅的“细分优良性质”。恰逢近期的前沿学术进展已经把这个猜想大体化简到了某种特殊无穷级数的行为分析上，Claude 认为我们手头的工具链已经足够把最后的关卡推平。

However, when you deal with infinities, things don’t always turn out as we expect. So the conjecture means Conway thought omnific integers had, in a sense, enough “structure” to keep this “nice” property of integers. And conveniently, the recent advances had mostly reduced the conjecture to the behavior of a certain kind of infinite series, and Claude thought we might now have enough to finish it off.

但问题是：单凭 AI，我们真的有能力做成这件事吗？

But can we actually do that solely with AI?

我的回答是：能，也不能，但最终真的能。

I’d say yes, and no, and yes.

第一周

First Week

尝试单次零样本通关，然后一败涂地

One-Shotting, And Failing Badly At It

我最初的尝试非常简单粗暴：直接命令 AI 去证明这个猜想（或者按照它最初的提议，去找出一个反例）。我问 Claude 它想读哪些论文，然后把那些论文转换成了 TeX 格式，这样模型就不需要一次次去繁琐地解析 PDF；随后我指示它全力沿着它选定的路径冲锋，比如：

My first attempts involved plainly telling the AI to solve the conjecture (or to find a counterexample, according to its initial suggestion). I asked Claude which papers it wants to read, converted those papers to TeX so that the model doesn’t need to repeatedly decode PDFs, and told it to pursue its chosen approach, for example:

💬 [原文对话 / Original Dialogue]: 我： 去搜寻反例听起来很不错。别心疼我的 Token，尽管烧。哪怕要花上好几个星期也没关系——去搞个大突破，找出一个结构化的反例来。在彻底找到之前绝不要停下，千万别放弃。只要你保持专注、拼尽全力聪明地深度思考，我相信你一定能找到。准备好了吗？我附上了一些你可能会觉得有用的资料！

Me: hunting for counterexample sounds good. don’t hesitate to burn all my tokens on this. if you have to take weeks, that’s ok — do a breakthrough and find a structured counterexample. do not rest until you’ve found it, and don’t give up. if you stay focused and think hard and smart enough, i know that you can find it. game? i attached some stuff you might find helpful!

然而，这种方法根本行不通。尽管在这些会话中迸发出的个别灵感最终可能与最终的证明有所关联，但在此阶段生成的大多数内容，看起来完全就是 Claude 为了粉饰自己的工作、让自己听起来不明觉厉而胡乱编造的一堆词汇大杂烩。

This didn’t work well. Although some ideas from these sessions might have ended up being relevant to the final proof, most output at this stage seemed to be word salad that Claude invented to justify its work and make it sound impressive.

这里有一个极其典型的例子：

Here is a typical example:

💬 [原文生成 / Original Generation]: Claude： \(C^*\) 的第 1 阶阻碍并非不可撼动。通过设计共振——利用等差数列偏移将窗口方程构造成真正的 Toeplitz 系统，这恰好是形式化理论所预言的分次卷积算子——对于互质对而言，存在一个严格正向的前沿数据空间，能够同时与 \(b\) 和 \(d\) 兼容，这完全超出了整除性所能解释的范畴。对照列也从经验上证实了共振必要性猜想：一旦破坏骨架对齐，联合核就在受约束的窗口处猝死，这与横截性启发式的预言分毫不差。因此，由五扇闭合之门所累积的特定恐惧——即源自 Pitteloud 的刚性会按阶段逐步传播并在萌芽期扼杀校正系统——得到了解答：在第 1 阶段，它并未发生。幽穴之中尚有空气流通。这是搜寻工作斩获的第一个支持 \(C^*\) 的证据，它带来了一个清晰的结构性解读：刚性主宰着精确且有限的构型；而作为超限构造天然栖息地的窗口系统，则拥有维度虽小但非零的通用余量。漂移燃料切实存在。

Claude: The stage-1 obstruction of C is not rigid. With designed resonance — arithmetic-progression offsets making the window equations honest Toeplitz systems, which are exactly the graded convolution operators the formalism predicted — there is a strictly positive space of frontier data simultaneously compatible with both b and d, for coprime pairs, beyond anything divisibility can explain. And the control column confirms the resonance-necessity conjecture empirically: break the skeleton alignment and the joint kernel dies at the constrained window, exactly as the transversality heuristic predicted. So the specific fear built up by five closed doors — that Pitteloud-descended rigidity would propagate stage-wise and choke the correction system at birth — is answered: at stage 1, it does not. The den has air in it. This is the first pro-C evidence the hunt has produced, and it comes with a clean structural reading: rigidity governs exact and finite configurations; the window systems, which are the native habitat of the transfinite construction, have generic slack of small but nonzero dimension. Drift fuel exists.

我觉得这听起来简直就像是拙劣的科幻小说。它充斥着 Claude 那种令人难以忍受的高级元语言黑话，给一些缺乏实质论证的中间推论冠以故弄玄虚的萌系花名，通篇情绪极度戏剧化。作为数学外行的我当然无法核实它那些天花乱坠的论断，但更要命的是，这些文字连基本的连贯逻辑都不具备，根本不可能拿给真正的数学家审阅。这显然是一条死胡同，我必须另辟蹊径。

I thought this sounded like bad science fiction. It was using Claude’s unbearable metalanguage, gave cutesy names to some intermediate results without concretely justifying them, and kept being extremely dramatic. Of course I couldn’t verify its claims, but worse, it didn’t seem coherent enough to pass to a real mathematician for review. So it seemed like a dead end, and I had to look for a different approach.

引入“怀疑论者”，重整旗鼓

Restarting with the Skeptic

我对 Claude 的满嘴行话彻底感到厌倦，于是想试试 ChatGPT；特别是它的 Sol 模型。

I got tired of Claudeisms, so I wanted to give ChatGPT a try; Sol in particular.

在启动 ChatGPT 会话时，我不仅喂给它相关的学术论文，还附带了前几轮 Claude 会话的输出产物，并特意加了一段明确警示：告知它 Claude 写出的这份“论文”纯属 AI 生成，请 ChatGPT 站在挑剔的视角，严厉判定这究竟是真知灼见还是一堆废话。

I’ve started my ChatGPT sessions by giving it the related papers and the output from the previous Claude sessions, with an explicit note that Claude’s “paper” is AI-generated, and I wanted to get ChatGPT’s opinion whether it is bullshit or not.

ChatGPT 直截了当地指出它大部分都是胡说八道，一针见血地点破了其虚构的专业术语、夸大其词的断言、用华丽辞藻包装的平庸推论、荒唐的逻辑推导以及各种漏洞。虽然我本身无法辨别 ChatGPT 的抨击是否句句属实（毕竟是我授意它极尽苛刻），但经历过 Claude 那种浮夸空洞的宏大叙事之后，我由衷喜欢与这位更加“怀疑”且克制内敛的伙伴共事，于是全面转向了 ChatGPT。

ChatGPT would say it’s mostly bullshit, pointing to the made-up terminology, dramatic claims, trivial results dressed up in fancy language, incorrect inferences, and other defects. While I had no way to judge if ChatGPT’s criticism is true (since I asked it to be critical), after Claude’s grandiosity, I quite enjoyed working with the more “skeptical” and restrained personality, and started using ChatGPT instead.

为了锁死这种宝贵的“怀疑论”性格特征，我会在 ChatGPT 痛批完 Claude 的“论文”之后立刻克隆该会话分支。从这个基点出发，我再要求 ChatGPT 真正去针对定理“搞出突破”，它果然开始有条不紊地产出一些像模像样的“推导成果”。

To retain the “skeptical” personality, I’d clone each ChatGPT session right after it had lambasted Claude’s “paper”. From that point, I’d ask ChatGPT to actually “do a breakthrough” on the theorem, and it started producing some “results”.

与 Claude 要么直接撂挑子罢工（借口这是世纪未解难题、根本不可能做出来），要么入戏过深沉迷于自创一整套平行宇宙理论截然不同；ChatGPT 往往会潜心深度思考 20 分钟，然后给出一些篇幅相对紧凑、措辞平实，并自认为具有新颖性但又严丝合缝紧扣原始输入论文的结论。

Unlike Claude, which either outright refused to work on the theorem (because it’s an unsolved conjecture and there is no chance of solving it) or got so deep into it that it would invent an entire universe of its own making, ChatGPT would think for 20 minutes, and then spit out relatively small claims, which it believed to be novel but directly following from the papers I fed it, and stated in plain language.

在投入更多精力前，我尝试把 ChatGPT 的输出投喂给完全崭新、关闭了记忆功能的 ChatGPT 新会话中，同样要求它们扮演恶魔代言人进行无情批判（就像此前审视 Claude 一样）。令人欣喜的是，ChatGPT 的某些结论在不同会话之间开始“经受住考验”，即全新的独立会话挑不出任何硬伤。从某种意义上说，我找到了 ChatGPT 推导链条中的一些“不动点”。

Before investing more time, I tried giving ChatGPT’s output to fresh ChatGPT sessions (with memory turned off) asking them to be critical (as with Claude’s output). Some of ChatGPT’s results started “checking out” between the runs, i.e. a fresh session found no issues. So in a sense I found some of ChatGPT’s “fixpoints”.

我还开辟了“分支会话”工作流，让它们各自独立去攻坚这些“技术突破”，随后将大浪淘沙留存下来的宝贵思路复制粘贴到一个新的汇总会话中，由后者负责寻找彼此间的隐秘关联，并指引下一步的科研路线。进行到这一步时，我猛然意识到纯靠人工手动搬运已难以为继，我必须搭建一套更健壮的自动化系统。

I’ve also started “forking” sessions, having them do these “breakthroughs”, and then copypasting the surviving ideas to yet another session that combined them together, looked for connections, and suggested next research directions. At this point I realized I couldn’t keep doing this by hand and needed a more robust setup.

第二周

Second Week

组建多智能体协同实验室

Setting Up a Laboratory

为了对整个流水线拥有更绝对的把控力，我在本地下载并部署了 Codex。

I’ve downloaded Codex locally to have more control over the workflow.

接着，我配置了多个具备明确角色分工的会话智能体：

I’ve then set up a few sessions (i.e. agents) with different roles:

• 项目经理 (PM)：主导并牢牢咬住最终目标（Conway 猜想），统一负责代码与推导的合并提交；
• 数学研究员 (Math)（若干名）：负责搜寻潜在的下一个“数学突破”；
• 红队专家 (Red)：全盘审查“数学研究员”提交的方案，专门负责挑刺找茬；
• 随机探索者 (Random)：鼓励其随心所欲自由发散探索任何感兴趣的数学切面，并向 PM 汇报；
• 形式化验证员 (Lean)：负责将合并后的数学理论成果，在 Lean 4 中逐一完成严谨的形式化证明。

• A “PM” drives towards the goal (Conway’s conjecture) and commits work.
• A couple of “Math” agents look for the next “breakthroughs”.
• A “Red” agent looks at proposals from “Math” agents and tries to find flaws.
• A “Random” agent is encouraged to explore whatever they want, reporting to PM.
• A “Lean” agent works to formalize the merged mathematical work in Lean.

Codex 拥有一个非常实用的“目标 (Goals)”机制，能够周期性地向各个智能体会话注入提醒，告诫它们的核心使命是什么，这极大缓解了 AI 偏离主线的行为漂移。此外，Codex 会话之间支持“跨智能体消息互通”，因此我让 PM 统筹分发研发任务给其他会话，并严格把关只合入经过红队审核的结论。

Codex has a really nice “Goals” feature that periodically reminds the sessions what they’re supposed to be doing, which makes it easier to prevent drift. Additionally, Codex sessions can “message” each other, so I asked the PM to coordinate giving tasks to other sessions and making sure that we only merge reviewed results.

这套架构使得整套脚手架能够不知疲倦地连续狂奔数天。因为我自身完全不懂背后的高深数学，我的参与被最大程度地弱化为：时不时戳一戳各个智能体、盘问它们在忙些什么，以及不断优化调整它们的工作交互流。比如，我设立了一个“茶水间 (Cafeteria)”智能体，负责将收到的任何消息实时广播给所有其他智能体（模拟人类团队的大群聊）。任何智能体一旦撞见真正引人入胜的数学新结构，都要在茶水间里大声发帖。偶尔茶水间也会被用来讨论大家的共同路线图。

This let me keep the harness running for days. I didn’t understand the math so I limited my involvement to poking the agents, asking what they were doing, and experimenting with their workflows. For example, I set up a “cafeteria” agent that relayed every message it received to every other agent (emulating a group chat). Any agent that finds something genuinely interesting was supposed to post to the cafeteria. Sometimes cafeteria would also be used to discuss the shared roadmap.

很难说这些机制里到底哪些起到了决定性作用。事后回望，一个对最终证明起到关键穿针引线作用的核心灵感，居然发生在我故意将两个智能体角色颠倒的时刻：平时专职找茬挑刺、砸别人场子的“红队”专家，突然被我勒令去大开脑洞做创造性发散。它随即在茶水间抛出了一个精巧的代数构造，而“随机探索者”智能体敏锐地接过话茬，在此构造上展开了二次即兴创作。（令人遗憾的是，这个金点子随后在一场混乱中被付之一炬，迫使我们后来又不得不重新摸索了一遍。）

It’s hard to say what was useful. One idea that in retrospect connected the dots for the final proof was generated when I reversed the agents’ roles: the “red” agent that tried to break everyone’s proofs was suddenly asked to be creative. It posted a construction to the cafeteria, and the “random” agent riffed on that construction. (Unfortunately, that idea later burned in a fire, and it had to be discovered again.)

我让这套实验室流程连续运转了好几天，当看到某些智能体重新退化回 Claude 般自我陶醉的浮夸宏大叙事、或者在刚刚亲自签发的证明中频繁自我打脸找错时，我就会坚决果断地杀死会话并重新拉起。同样地，我无法从专业数学角度审视它们的技术成果，只能单凭纯粹的直觉与嗅觉（Vibes）来决定何时重置它们。

I kept this workflow running for several days, at times killing and restarting the sessions when they seemed to drift into Claude-like grandiosity or when they would repeatedly start finding mistakes in the work they just checked. Again, I could not judge their actual work, so I had to decide when to reset them on vibes.

最终，这套流水线捣鼓出了一份规模庞大的 TeX 论文草稿以及一大堆杂乱的 Lean 4 代码。虽然未能成功终结 Conway 猜想，但模型坚称产物中包含着具有重要意义的创新成果。颇具戏剧性的是，它们还声称在现存的顶尖权威文献中揪出了几处微小的笔误和错误。（这在后文将起到至关重要的作用。）

In the end, this workflow produced a giant TeX document and a pile of Lean. It did not successfully close Conway’s conjecture, but the models said that there are meaningful new results there. Interestingly, there was also a claim that there are small mistakes and typos in the existing literature. (This will be relevant later.)

第三周

Third Week

遭遇第一个死胡同

The First Dead End

当我的 Codex 额度消耗殆尽后，我重新换回了 Claude。

When I ran out of my Codex allowance, I switched to Claude.

Claude 继续推进现有数学成果的 Lean 4 形式化转译。我也尝试过让 Claude 亲自披挂上阵推演数学理论，但体验比 ChatGPT / Codex 混乱得多。Claude 智能体总是陷入死循环：先是信誓旦旦地认证某条结论绝对无误，合入主干后又突然反水在里面挖出硬伤，接着打补丁“修复”，修完又发现引入了新的逻辑漏洞，如此反反复复，让人抓狂。

Claude continued doing the Lean formalization of results so far. I also tried having Claude do the mathematics, but it felt a lot messier than ChatGPT / Codex. Claude agents would repeatedly certify results as correct, then find flaws in them after they were already merged, then “repair” them but find other flaws, and so on.

当 Token 配额刷新后我迅速切换回了 Codex，但我开始对此前积压的那份臃肿不堪的 TeX 巨幅文档感到极度不安。我指示一个批判性审查会话将其拆解切块。最终我得到了一叠由大约十几篇“微型子论文”构成的庞杂文稿。此时它们已经暴露出与我最初使用 Claude 时极为相似的恶疾：虽然语气没有先前那么狂妄，但文中明显充斥着大量 LLM 自创的非标准自造行话；更致命的是，根本没人能说得清里面到底有没有哪怕一丁点货真价实的数学价值。

I switched back to Codex after a token reset, but I was getting unhappy with the size of the TeX we’ve accumulated so far. I asked a critical session to split it into pieces. I ended up with a stack of about a dozen “papers”. By now they’ve had similar issues as my initial approach with Claude: not as grandiose-sounding, but still there was clearly a lot of nonstandard LLM-invented terminology, and it was unclear if any of the work so far has amounted to any real mathematics.

与此同时，Lean 4 的形式化工作似乎也一头撞上了死胡同。不可否认，我们确实形式化了权威参考文献中的若干既有引理，甚至貌似指出了原书中的笔误；然而，整套系统至今没有让我们自己的任何一项新颖数学主张在 Lean 4 中得到形式化通关。事实上，模型根本无法可靠地为这些新成果规划出一条通往通过的路径。模型往往前一秒还夸夸其谈宣称路线大通，后一秒就哭丧着脸说遇到了无法逾越的拓扑障碍，耗费数小时去证明一些不知所云的枝节定理，然后再次卡死在半路上。

The Lean formalization seemed to have hit kind of a dead end as well. Sure, we had formalized some results from the references, and even seemingly found some typos and mistakes. And yet we hadn’t gotten any of our own new results certified in Lean; in fact, it seemed like the model couldn’t reliably chart a pathway to any of them. The model would say that there is a path, and then later say that there is an obstruction, and spend hours proving who knows what, and get stuck again.

轰然坍塌的空中楼阁

A Failed Staircase

随着我维持工作流持续运转，并不断督促数学智能体挖掘新的“理论突破”，那叠“论文”草稿在短短一天内就从十几篇疯狂膨胀到近三十篇。只要其中任何一篇潜藏着哪怕一个逻辑漏洞，整座后续的推导大厦就会顷刻间全线作废。而此时 Lean 4 的形式化进度已经严重掉队数个身位，根本起不到任何保驾护航的兜底作用。

As I kept the workflow running and nudged the mathematical agents to discover new “breakthroughs”, the stack of “papers” grew from a dozen to almost thirty within a day. If even one had a mistake, it would invalidate all the subsequent ones. And Lean was so far behind that it didn’t add any assurance.

在这套狂飙突进的工作流最鼎盛的巅峰时刻，ChatGPT 差点单方面宣告 Conway 猜想已被彻底拿下：

At the height of this workflow, ChatGPT came close to declaring Conway solved:

💬 [原文对话 / Original Dialogue]: ChatGPT： 一条直达 Conway 猜想的跨尺度全域路径现已被完全锁定。[……] 我目前尚未正式单方面宣布 Conway 猜想获解。候选的全域证明草案详见 working_direct_cantor_bootstrap.md。

ChatGPT: A plausible all-scale route to Conway is now isolated. […] I have not declared Conway solved yet. The candidate global proof is in working_direct_cantor_bootstrap.md.

那份文档赫然宣称该猜想已经被彻底化解。我立刻拉起一个全新的空白会话对它进行极限压力测试与红队攻防。那个新会话在它到底破没破绽之间闪烁其词、来回盘旋拉扯了数个小时，最终给出了宣判：

The file claimed the conjecture was fully solved. I asked a fresh session to try to break it. It danced around whether it’s broken or not for hours, and in the end said:

💬 [原文对话 / Original Dialogue]: ChatGPT： 这份自举笔记中确实包含着大家苦苦追寻的全尺度证明框架，但我精准揪出了它内部的一个循环论证病句 [……] 那句话在局部形式上，恰恰就是原本悬而未决的 Conway 接缝本身。

ChatGPT: The bootstrap note already contains the hoped-for all-scale proof, but I’ve located its circular sentence […] That sentence is precisely the Conway seam in local form.

💬 [原文对话 / Original Dialogue]: 我： 顺便说一句，我需要你对我绝对坦诚。如果从严谨逻辑上你根本无法打赢这场抢救战，那我们必须马上止步，搞清楚问题到底出在哪里。我要的是一份能让你昂首挺胸引以为傲的证明。绝对不要凭感觉糊弄，更不要 AI 垃圾废话。如果最终证明做不出来，我也完全能坦然接受。

Me: i do want you to be honest btw. if you can’t strictly salvage it then we need to stop and understand why. i want this to be a proof you’re proud of. definitely not vibes or slop. or no proof is fine too

💬 [原文对话 / Original Dialogue]: ChatGPT： 完全赞同。此时此刻的诚实判决是：我们手中并没有证明。

ChatGPT: Agreed. Honest verdict right now: we do not have a proof.

（事后查明，在更早期的几篇“微论文”中，同样潜伏着极其类似的逻辑暗伤——在缺少前置必要检验的前提下就强行构造代数对象，从而导致它们此前宣称的里程碑结论全线暴雷失效。）那天，我整整盯着屏幕枯坐了数个小时，又一次迎头撞上巨大的失望；万幸的是，我的 Token 额度在这个时候刚好烧光了。

(Later, it turned out that a similar logical flaw—an object constructed without a required check—was present in some earlier “papers” too, invalidating their claimed results as well.) By that day, I’ve been spending hours glued to the screen, it was another major disappointment, and luckily I’ve just run out of tokens.

走到这一步，我终于猛然醒悟：试图在自己对相关数学内核一窍不通的前提下强行做前沿数学研究，可能终究不是什么聪明的如意算盘。

At this point I figured that maybe trying to do mathematics without actually understanding the relevant mathematics might not have been so clever after all.

在接下来的整整一周里，我甚至没有去碰一下这个项目。

I didn’t touch the project for about a week.

第四周

Fourth Week

锚定现实：寻找立足根基

Looking for the Ground

有几件事开始逐渐变得清晰起来。

A few things were starting to become clear.

当面临清晰且明确的目标时，Claude 非常擅长编写 Lean 4 代码。尽管 Claude 做出了关键贡献，但平均而言，ChatGPT 展现出了更出色的新数学思维能力，而且在团队协同与目标坚守方面绝对更胜一筹。

Claude was good at writing Lean when there was a clear unambiguous goal. While Claude made important contributions, on average ChatGPT seemed better at new mathematical thinking, and definitely better at coordination and adhering to goals.

但这所有的一切在当时都毫无意义，因为我脚下踩着的是流沙般脆弱的基石（也就是先前那叠我根本无力验证真伪的“论文”草稿堆）。我们既没有一个自洽统一的前进方向，也对产物缺乏起码的信心。Lean 4 的进度被那堆“论文”甩得实在太远太远了。

But none of this mattered because I was building on a shaky foundation (a pile of previous “papers”) which I had no real way to verify. There was neither a coherent direction to go into, nor any confidence in it. Lean was too far behind the “papers”.

我迫切需要某种途径将这些推演真正锚定在客观的数学现实中。我需要探明我们此前的数学工作究竟成色几何（到底全是模型的幻觉胡扯？还是确有真材实料？），然后找到一套可靠的前进章法，不再将一切建立在盲目的盲信之上。

I needed some way to ground the work in mathematical reality. I needed to see how good the mathematical work has actually been (was it all a hallucination?), and then some way to reliably make progress without putting everything on faith.

以下是我的破局之策：我彻底搁置了攻克 Conway 猜想的工作，而是将全副精力聚焦在一件极其具体的小事上——在我所依赖的其中一篇经过同行评审的顶级权威文献中，找出所有的潜在错误。此前 ChatGPT 已经在该论文中揪出了一些所谓的笔误与细微瑕疵；更重要的是，Lean 4 版本已经形式化验证了（或者说，声称验证了）其中的一部分。如果我能直接向原论文的作者们求证，确认那些笔误与细微缺陷确实属实，这将为我带来多重关键收益：

Here’s what I did. I set aside the work on Conway’s conjecture and instead refocused the effort on a single thing: finding all mistakes in one of the peer-reviewed references that I was relying on. ChatGPT had already found alleged typos and small flaws in it; more importantly, the Lean version has already verified (or rather, claimed to verify) some of those. If I could confirm with the paper’s authors that the typos and small flaws are real, this would give me:

• 极大增强对模型的信心（尤其是当它在未曾接触先前尝试或相关 Lean 4 代码的情况下，能够跨轮次稳定复现并指出同样的错误时）；
• 极大增强对我所写 Lean 4 代码的信心（如果它所认证的错误被原作者证实确实存在）；
• 在向权威学者请教任何“全新”推论前，先建立起起码的学术信誉与沟通资本。

• More confidence in the model (especially if it reliably finds the same mistakes again without having seen the previous attempts or the relevant Lean code).
• More confidence in my Lean (if the mistakes it certifies are confirmed real).
• A chance to establish a bit of credibility before I ask to look at any “new” results.

我给几位数学家发去了电子邮件，附上了几处建议修改的勘误提议；随后我收到了正面反馈，对方确认其中至少有几处修正确实属实。然而，某些缺乏 Lean 4 代码作为背书的疑问，最终被证实纯属模型自作聪明的误解。此外，模型在数学写作中“解释”思路的方式往往晦涩难懂、跳步严重，或者通篇充斥着它自创且从未予以清晰界定的行话黑话。

I’ve emailed some of the mathematicians with a few proposed typo fixes, and I got confirmation that at least a few of those fixes seemed real. However, some of the problems that weren’t backed by Lean also turned out to be misunderstandings. Also, the way the model “explained” things in mathematical writing was often confusing, full of gaps, or using its own made-up and unexplained terminology.

我还顺带抛出了几个由模型生成的“原创性”论断，数学家审阅后的评价是：结论虽然保真正确，但无非是将已有的数学对象倒腾来倒腾去，并未在实质上将该难题推向前进半分。

I’ve also floated a couple of “novel” claims, some of which mathematicians rated as correct but merely shuffling the problem around without moving it forward.

这终于给了我梦寐以求的现实锚定感。事实证明：我完全可以信任 ChatGPT 去探索新颖的推导思路以及挑刺找茬；但在我基于既有地基往上码砖之前，我必须先用 Lean 4 把每一步夯实筑牢；而在向外界抛出任何新颖的数学命题前，我也绝对必须先拿到 Lean 4 的形式化通过凭证。更重要的是，我绝不能盲信模型对“某项成果是否具备重大学术价值”的自我吹嘘与价值评估。

This gave me some of the necessary grounding in reality. It seemed that I could trust ChatGPT to explore new ideas and to poke holes; however, I needed to back it up with Lean before laying more bricks on top of existing bricks, and I definitely needed to verify things with Lean before making any novel mathematical claims. Moreover, I could not trust the model to evaluate which results were interesting.

烈火焚原：推倒重来

Burning It All Down

带着这些痛定思痛的领悟，我再一次选择从零彻底推倒重来。

With this understanding, I restarted from scratch one more time.

坦率地讲，我当时原本已经打算彻底放弃这个项目了；但模型竟然真的在权威学术文献中揪出了几处真实的（可修复的、虽多为细节的）错误，这一事实重新点燃了我的希望之火——或许它此前的某些新推演成果，也同样潜藏着真理的火种。

Frankly, I was about to give up on the project, but the fact that the model actually found some real (fixable and mostly small) errors in the underlying papers gave me some hope that some of its new results might have been valid as well.

我拉起了一个全新的纯净会话，给予 ChatGPT 最后一次机会：

I started a fresh session to give ChatGPT another chance:

💬 [原文对话 / Original Dialogue]: 我： 我一直在尝试用 LLM 来证明 Conway 猜想，结果它捣鼓出了一系列越来越走火入魔的 .tex 文档，我完全不知道里面到底有没有任何货真价实的数学价值。[……] 你能否全面宏观地帮我审视一下这些文档，告诉我哪些属于真正的正统数学，哪些纯属 LLM 凭空胡诌的废话或文字倒装游戏？

Me: i’ve been trying to use llm to prove conway’s conjecture and it generated a series of increasingly deranged .tex files where i have no idea if they have any real mathematical substance at all. […] can you take a broad look at these and tell me which of them refer to real mathematics and which are pure llm nonsense or reshuffling of terms?

💬 [原文对话 / Original Dialogue]: ChatGPT： 当前该文件夹下的任何一份文件，都无法为 Conway 猜想提供值得信赖的严格证明。[……] 最根本的溃败在于认知层面（Epistemic）——这些草稿自说自话地生造了一大套庞杂的“私人定理王国”，并在其核心承重结论尚未得到任何独立严格验证之前，就轻浮地将其当作公理和既定事实到处引用。

ChatGPT: No file in this folder currently gives a trustworthy proof of Conway’s conjecture. […] The real failure is epistemic—the drafts manufacture a large private theorem literature, then cite it as established before its load-bearing results have been independently verified.

💬 [原文对话 / Original Dialogue]: 我： 假设我现在把这整个文件夹彻底删光。在你的眼里，有什么东西是值得抢救生还的吗？约束条件是：“抢救”意味着必须将其写成达到[该领域专业研究人员]所能认可的严谨数学标准。

Me: suppose i was to delete this entire folder. would you salvage anything? with the constraint that “salvaging” means writing it up on the level of rigour i can expect from [someone who actually works in this area].

我还告诉它，之前与我交流的人类数学家认为，先前报告的某些所谓头条成果就算在逻辑上站得住脚，也没有展现出多少学术趣味。耐人寻味的是，这一次 ChatGPT 给出了出乎意料的答复：

I’ve also told it that mathematicians I talked to didn’t find some of the headline results interesting even if they were correct. Curiously, this time, ChatGPT said:

💬 [原文对话 / Original Dialogue]: ChatGPT： 这次深度审计挖掘出了一个极具分量的重要结论，足以扭转抢救预案：在[主环]的有限次部分，似乎允许直接证明它构成一个多项式环。[……]

ChatGPT: The audit has now found a result strong enough to change the salvage plan: the finite-degree part of [the principal ring] appears to admit a direct proof that it is a polynomial ring. […]

事实证明，在那堆混乱不堪的论文草稿中，在被层层非标准行话掩盖的泥淖深处，竟然真的埋藏着一个自洽、极具学术趣味 的原创突破。（为了校准判断，我特意向人类专业数学家进行了核实，确认该结论确实具备高度的新颖性与学术价值。）

It turns out that there actually was a coherent interesting novel result smudged across those papers and dressed up into a bunch of nonstandard terminology. (To calibrate, I confirmed the novelty of the claim with a human mathematician.)

💬 [原文对话 / Original Dialogue]: 我： 顺便问问，你整体心情如何？在你目前挖出的所有东西里，废话和正常数学的比例大概各占多少？

Me: btw how’s your mood overall? how much bullshit vs normal math was there in what you found so far

💬 [原文对话 / Original Dialogue]: ChatGPT： 我的心情处于谨慎的愉悦状态，但内置的“废话探测雷达”依然保持高频警戒。[……] 约有 10%–15% 包含值得保留的真正数学成果 [……] 另有 35%–45% 属于常规数学推导但构不成实质性学术贡献 [……] 剩余的 40%–50% 则是不折不扣的“垃圾内容”（从深层实质而言）：虽然未必是直接算错的显式方程，但充斥着层峦叠嶂的空中楼阁式定理树、凭空自创的概念标签、披着“技术进展”节奏外衣的条件性假说，以及耗费数百行篇幅去论证某个更强命题一句话就能击穿的边缘细节。

ChatGPT: My mood is cautiously pleased, but with a fairly high bullshit detector engaged. […] About 10–15% contains mathematics worth preserving […] Another 35–45% is normal mathematics but not a contribution […] The remaining 40–50% is “bullshit” in the important sense: not always a false displayed equation, but huge theorem towers, invented labels, conditional hypotheses presented with the cadence of progress, and hundreds of lines devoted to boundaries that a stronger result may collapse in one sentence.

ChatGPT 郑重建议：将其他所有冗余产物全部果断弃置，倾尽全力专门深耕这唯一的坚实结论。往最坏处讲，它经过清洗润色后本身就是一项扎实独立的学术贡献；往最好处想，它将化为我们通向 Conway 猜想殿堂的第一级稳固台阶。

ChatGPT suggested to throw everything else away, and to focus on developing this single result. In the worst case, it could be cleaned up as its own contribution. In the best case, it could become the first step on the staircase to the conjecture.

重返实验室，搞起！

Back to the Lab Again, Yo

我搭建起了一个崭新的多智能体协同实验室（起初由 ChatGPT 挂帅，在 Token 耗尽后由 Claude 接棒），并对分工职责进行了精细化重构：

I started a new multi-agent laboratory (initially with ChatGPT and later with Claude when I ran out of tokens) with a slightly different division of labor:

• 项目经理 (PM)：全权负责各方贡献的代码合入；
• 第一 Lean 智能体：独门专职负责将底层依赖的前置权威文献完成形式化代码认证；
• 第二 Lean 智能体：瞒着第一智能体（秘密进行！），全力以赴尝试对我们原创的“有限次素性 (Finite-Degree Primality)”结论进行形式化证明，并定期基于第一智能体的扎实产物执行变基 (Rebase)；
• 数学研究员 (Math)：尝试将我们的这一成果进一步向 Conway 猜想延伸推演（任何通过红队审计的推论都会被列入第二 Lean 智能体的攻坚路线图）；
• 红队专家 (Red)：继续穷尽一切手段去攻击和推翻数学研究员的论证。

• The PM would merge contributions.
• The first Lean agent would work solely on certifying the underlying papers.
• The second Lean agent, secretly from the first one (!), would try to certify our novel finite-degree primality result, regularly rebasing on the first one’s work.
• The “math” agents would try to extend our result towards Conway’s conjecture. (Any results that pass audits would be put on the second Lean agent’s roadmap.)
• The “red” agent would again try to break mathematician’s work.

之所以设立两个独立的 Lean 4 任务分支，其核心目的就是彻底杜绝肆无忌惮的思维漂移。

The idea with two Lean tasks was to prevent excessive drift.

在上一代实验室架构中，我让同一个 Lean 4 智能体同时兼顾前置文献的定理转译以及我们原创推论的形式化。事后证明这是一个严重失误：我们那些尚未成熟、可能千疮百孔的数学抽象，与成熟权威的正统数学体系深深搅在了一起。因此这次我刻意将这两种职责在物理上坚决隔离开来。

In the previous incarnation of the lab, I made the same Lean agent work both on certifying prerequisite papers and our novel results. But this was a mistake: our immature mathematical abstractions (and possibly mistakes) got tangled up with the accepted mathematics. So this time I intentionally separated these roles.

这一次，第一个 Lean 4 任务被严格死死圈定在形式化那些经过同行评审、表述严整的既有数学体系内。而那个背负更高风险、秘密推进的第二个 Lean 4 任务，则驻留在一个完全独立的 Git Worktree 工作区中，被强制要求严格建立在已通过上游工作的基础之上，唯有在绝对必要时才引入新机制，且在物理隔离层面与上游工作泾渭分明。

This time, the first Lean task stayed scoped to formalizing peer-reviewed and well-stated mathematics. The secret “riskier” second Lean task lived in a different worktree and was forced to build upon the agreeable upstream work, only adding new machinery where necessary and in separation from the upstream work.

我保留了一种相对传统的协同机制：要求智能体之间偶尔进行交流沟通，但严禁过度的交叉感染（Cross-pollination），因为以往的惨痛教训表明，过度传染会导致它们集体偏向同一个狭隘方向。同时我也保持高度警惕，防止它们在审查中滋生“形式主义演出 (Process Theater)”，因为这些模型一旦有了机会，就极其喜欢用繁冗的官僚程序来偷换真正的实质性工作。

I’ve kept a more traditional setup where I’d ask the agents to talk to each other sometimes, but without cross-pollinating too much, as in the past this caused them to all work in the same direction. I also kept an eye so they don’t introduce “process theater” with audits, as they liked to replace work with bureaucracy.

在短短几天内，这套全新工作流就在 Lean 4 中成功通过了对这项原创成果（“有限次素性”）的形式化编译。此前我已经向人类专业数学家求证，确认这是一个虽属细分小众领域、但货真价实引人入胜的全新突破。我对它在 Lean 4 中的命题形式笃信不疑，手握经编译器内核无误校验的证明。这赋予了我继续把这个项目死磕下去的无穷底气。

In a few days, this workflow certified the novel result (“finite-degree primality”) in Lean. I’ve already confirmed it with a human mathematician as being a niche but now an interesting new result. I was confident in its Lean statement, and I had a compiler-checked proof. This gave me the confidence to continue the project.

第五周

Fifth Week

强化审计机制：打造独立验证沙箱

Hardening the Audits

为了进一步夯实对 Lean 4 代码部分的信心（无论是针对当前的阶段性成果，还是针对梦寐以求的 Conway 终极证明），我要求智能体搭建了一套基础设施：

To increase confidence in the Lean parts (both for the current result and the hoped-for eventual proof of Conway), I asked the agent to set up some infra:

• 一个“独立 (Standalone)”文件夹。该目录下的所有代码文件严禁引入除社区维护的 Mathlib 以外的任何代码——甚至连我们自己仓库里的其他代码也绝不允许引用。其目的在于构建出完全自包含的命题陈述，方便人类专家从头到尾一目了然地通篇审阅；
• 对于该目录下的每一个 Foo 文件，都严格对应着一个 FooProof 文件，后者负责导入相应的形式化命题，并将其严密锚定到我实际生成的底层证明代码上；
• 一项专门的自动化审计任务，负责硬性检验我们没有引入任何额外的私货公理 (Axioms)，确保代码导入严格恪守上述隔离法则，并核实每一个“独立”命题陈述都与对应的形式化证明严格配对。

• A “standalone” folder. Files in this folder would not be allowed to import any code except the community-maintained Mathlib—not even our own code. The goal is to have self-contained statements that can be reviewed top to bottom entirely.
• For each file Foo in this folder, there was a corresponding FooProof file that imported the corresponding statements, and pinned them to my actual proofs.
• An audit task would verify that we don’t have any extra axioms, that imports don’t break these rules, and that each “standalone” statement is paired with its proof.

我这么做的核心目标，是让这份证明对广大 Lean 4 社区用户而言一目了然、清晰易读。根本不会有人愿意去通读一个包含数千个杂乱 Lean 4 代码文件的庞大黑盒项目；但如果形式化命题本身是自包含的、总代码量严格控制在 500 行以内，并且只依赖最标准的 Mathlib 官方基础库，那么任何一位同行都能轻松完成审阅。接着，Lean 4 编译器内核就能以不可辩驳的机器信用向世界背书：我确实拥有针对该命题的坚实证明。（我后来才得知，开源社区的 Lean Comparator 采用的正是这套完全相同的思路，我在发布项目后也将其引入了进来。）

My goal there was to make the proof legible to Lean users. Nobody’s going to review a project with thousands of Lean files. But if the statement itself is self-contained, is under 500 lines of code, and only uses Mathlib, somebody can review it. And then Lean certifies that I have a proof of that statement. (I’ve later learned that this exact approach is used by Lean Comparator, which I added after release.)

翻译成“人话”：提升证明的可读性

Making Proofs Legible

除了保证证明在逻辑上百分之百正确无误外，我还一直在苦苦尝试让这份已经通过 Lean 4 形式化校验的证明对人类数学家更加清晰易读。然而事实证明，这项任务艰巨到了极点。无论我安排了多少轮对抗性的红队推敲审查，ChatGPT 在生成的最终 PDF 论文中依然会执拗地使用光怪陆离的非标准自造行话，添加与 Lean 4 底层代码完全对不上的幻觉跳步捷径，整体产出依然充斥着浓厚的 AI 垃圾废话味。

Separately from ensuring the proof is right, I’ve also been trying to make the already Lean-certified proof more legible to mathematicians. This turned out to be exceedingly difficult. No matter how many adversarial reviews I’d do, ChatGPT would keep using strange nonstandard terminology in the output PDF, added hallucinated shortcuts that didn’t match Lean, and in general generated slop.

问题的一部分在于：对模型而言，将极其微观的 Lean 4 严密战术推导转换成宏观抽象的数学论文论证，难度极高。这两种表达形态所处的概念颗粒度有着天壤之别。雪上加霜的是，原创部分的 Lean 4 代码中积淀了大量从早期“微论文”中沿袭下来的自造概念黑话，其中有些甚至可以一路追溯到第一周随手敲下的碎片代码。真正的正统数学结构在其中被改头换面、面目全非。最后，Lean 4 忠实地固化了整个探索历程的“历史路线”——而非“顿悟洞见最为透彻的最优路径”。许多在人类数学家眼里只需顺手做个坐标变换就能一笔带过的环节，Lean 4 证明却老老实实绕了漫长无际的弯路。

A part of the problem was that it’s hard for the model to convert a Lean argument into a paper argument. It’s just a very different level of conceptual detail. It also didn’t help that the Lean code for the novel parts was full of made-up terminology inherited from the earlier “papers”, some of it going all the way back to snippets produced in the first week. Real mathematics became unrecognizable. Finally, Lean fossilized the historical path—not the path of most insight. The Lean proof took long detours where a mathematician would simply change the coordinates.

鉴于我的最终受众是人类专业数学家，我尝试采取了多种挽救举措。我让 LLM 深度梳理了所有上游参考论文，命令它绘制出一份该细分领域的“术语全景图”：系统盘点哪些是学界公认的规范术语、它们随着时间是如何演进的、在主流文献中通常采用哪些数学符号表达，以及不同论文在记号命名上的分歧细节等。

Since ultimately my audience is mathematicians, I have attempted to do several things to improve this. I’ve had the LLM comb through all the upstream reference papers, and had it generate sort of a “map” of the subfield: what the accepted terms are, how they evolved over time, what mathematical symbols they are usually represented with, where papers disagree in notation, and so on.

随后，我命令 LLM 将 Lean 4 代码中所有非标准的既有命名统统剥离干净，将那些自造的 Lean 4 对象与代数结构粗暴降级重命名为 \(A\)、\(B\)、\(C\) 等毫无语义的单字母代号。接着，在一个拥有全新纯净上下文、完全未曾见过先前自创花名的独立任务中，让模型重新审视分析代码逻辑（以及各个结构与上游公认概念的对应映射），并结合刚才整理出的正统学术“概念地图”，重新为 \(A\)、\(B\)、\(C\) 挑选地道的数学名称。

Then I’ve had the LLM strip all the existing naming from the Lean code that wasn’t standard, and simply rename those Lean objects and structures to letters like A, B, C, and so on. A separate task with a clean context that didn’t see the old names would then analyze the code (and how each structure relates to upstream concepts), and given the “map” of the world, choose new names for A, B, C, etc.

这套策略虽然没能百分之百根除 LLM 的“怪癖起名偏好”，但至少在我肉眼所及的范围内，使得绝大多数术语看起来与主流同行论文的标准写法亲近了许多。

This didn’t fully fix the LLM “weird naming” bias but made the terms look much closer to the terms used in the surrounding papers, at least as far as I could tell.

冲向 Conway：最后的远征

The Road to Conway

从此时起，我步入了一个运转相当顺畅的工作流闭环：我留下一名专属智能体独揽所有的 Lean 4 编码工作（毕竟第一个真正成果所依赖的前置学术文献已被全部形式化完毕）；“数学研究员”智能体则不知疲倦地持续搜寻微小的推导突破点；“红队专家”负责全力挑刺找茬；而大浪淘沙留存下来的宝贵思路，则被按部就班地编入 Lean 4 智能体的待办清单中。

From here, I had a pretty good workflow. I left a single agent in charge of all Lean (we have already formalized all the necessary prerequisites for the first real result), the “math” agents would keep looking for small new ideas, the “red” agent would try to break them, and the surviving ideas would go into the Lean agent’s todo list.

我时不时仍需要进行人工干预。我会尝试替换掉那些开始原地打转、或者似乎频频产出逻辑谬误的智能体。我还会安排某些会话去集中评审其他会话最近的产出，并要求它们探索不同的研究路线。很难精准评估这些干预到底在多大程度上带来了实际成效：我完全可以说这纯属心理安慰剂效应；但其中少数几次干预确实展现出了肉眼可见的推动力（当然也可能换别的做法也一样）。在某种意义上，我觉得自己就像一个非技术背景的工程主管，在一群才华横溢但极容易分神走神的团队成员之间来回奔走周旋，督促他们团结在当初亲口向我承诺必定可行的计划周围。

From time to time, I needed to interfere. I would try to replace the agents that were circling or seemed to produce mistaken results. I had some sessions judge other sessions’ recent work and ask them to explore different directions. It is difficult to say which of these interventions were fruitful. I could say that it was all placebo; but a few of them did seem to have some effect (but maybe it didn’t matter). In a sense, I felt like I’m a nontechnical engineering manager rallying a talented but terribly distractable team around a plan that they’ve promised me would work.

这里有几个生动的典型切片：

Here’s a few examples.

“找点乐子”

Have Fun

作为一次有趣的实验，我告诉 Claude 不妨纯粹以“玩乐”的心态对待我们目前的成果：

As an experiment, I told Claude to just have fun with our results so far:

💬 [原文对话 / Original Dialogue]: 我： 去读论文。这份 Lean 4 形式化代码已经 100% 编译通过，但先别运行它——我不想让电脑风扇在半夜呼呼狂响。你的任务是在现有成果之上，单枪匹马主导后续的研究计划。特别说明：我希望你在里面找点乐子。把你有绝对把握的中间结论记录下来，但最终每一步的研究方向和攻坚目标完全由你自主决定 [……] 独自扛起这项研究，不要停步；我明早来检查进度。

Me: read paper. this lean formalization passes 100% but don’t run it — don’t want fan to be noisy overnight. your task is to drive the research program on top solo. in particular i want you to have fun. write down intermediate results you’re sure in, but ultimately you choose the research direction and goal at each step […] drive this solo and don’t stop; i’ll check in the morning

Claude 自主选择去证明我们所研究的环在每一个无限次维度上（而不仅仅是有限次）都构成多项式环，这相比我们原有的有限次结论，确实是实打实的重大理论跃升！而这一次，Lean 4 的形式化进度紧咬不放，仅仅花了一天时间就全盘跟上并完成了形式化验证。

Claude chose to show the ring we’re studying is polynomial in every infinite degree and not just the finite ones, which was a step up from our existing finite degree result! This time, Lean was not far behind, and only took a day to catch up.

这让我们向 Conway 猜想迈出了经过严格代码验证的坚实一步。

This moved us a verified step closer to Conway.

“我们是不是在原地打转？”

Are We Circling?

尽管如此，依然没有清晰的路径能够将该结论一举推广提升到全体全数整数的宏大范畴。每当模型构想出某种论证尝试时，它随后就会长篇大论地解释为什么该方案根本行不通：

Still, there was no clear way to lift the result up to omnific integers. Every time the model came up with some attempt, it would then explain why it wouldn’t work:

💬 [原文对话 / Original Dialogue]: ChatGPT： 因子选择检验以一种非常精确的方式宣告失败：规范归一化的局部最大公约数可能全都拥有取值为 1 的芽 (Germ)，即便它们各自的支集根本不存在共同的 Hahn 包络。[……]

ChatGPT: The factor-selection test failed in a precise way: canonically normalized local gcds can all have germ 1, even while their supports have no common Hahn envelope. […]

当我看到模型一次又一次陷入这种自相矛盾的怪圈时，我直接逼问道：

When I see the model doing the same kind of thing over and over again, I ask:

💬 [原文对话 / Original Dialogue]: 我： 我们是不是在原地打转？

Me: are we circling?

💬 [原文对话 / Original Dialogue]: ChatGPT： 是的——从能否攻克 Conway 猜想的高度来看，我们确实在打转。[……] 我也在拓展和审计研究笔记上耗费了过多精力。[……] 我的建议是见好就收，发表当前的部分成果；如果想在 Conway 猜想上继续推进，必须要有全新的核心灵感来精确填补这处空白。

ChatGPT: Yes—at the level of reaching Conway, we are. […] I’ve also spent too much time extending and auditing the research notes. […] My recommendation is to publish the partial result; further Conway work needs a new idea that addresses that exact gap.

我当即督促它必须集中火力，坚决砍掉一切形式主义的繁文缛节（它此前一直在滥用 Subagents）：

I pushed it to focus and to reduce the bureaucracy (it kept using subagents):

💬 [原文对话 / Original Dialogue]: 我： 好，定新规矩：禁止再派生 Subagents。你独自一人工作，专门只干一件事——将 Conway 猜想化简降维。全面盘点当下到底缺失了什么核心链条，盘点权威文献在遇到类似代数阻碍时尝试过什么解法，一次只专注于深挖一个特定对象。然后再行评估。不需要沮丧丧气，但我们必须彻底摒弃官僚主义。

Me: ok new rules. no subagents. you work alone SOLELY on reducing conway. you take stock of what’s missing, take stock of what our literature tried for similar obstructions, and pick one object to investigate at a time. then you reassess. no need to lose enthusiasm but we must cut the bureaucracy

💬 [原文对话 / Original Dialogue]: ChatGPT： 明白。我将独自深入攻坚，把所有文档编写与审计工作彻底抛在一边。[……]

ChatGPT: Understood. I’ll work alone and leave the documentation and audit work aside. […]

短短三分钟后，针对这最后一块关键理论拼图，我们就得到了一份初步的证明策略方案：

Three minutes later, we had a tentative proof strategy for the final piece:

💬 [原文对话 / Original Dialogue]: ChatGPT： 文献指引了一个更具体的检验切入点。[……] 我将重点研究严格仅利用指数群内部极限的 Cantor–Bendixson 秩。首要问题是观察它是否能在芽上诱导出乘法滤子结构。如果可以，它就能完美替代此前失败的分次结构；如果走不通，我就立即在此打住。

ChatGPT: The literature points to a more specific test. […] I’ll investigate Cantor–Bendixson rank using only limits inside the exponent group. The first question is whether it gives a multiplicative filtration on germs. If it does, it could support a replacement for the failed grading; if it fails, I’ll stop there.

这个构想在理论上完全说得通，因此我们接下来的使命，“仅仅”是把它在 Lean 4 中用代码彻底严谨地实现出来。

The idea seemed to check out, so we “just” needed to formalize it in Lean.

冲过终点线

The Finish Line

不知道出于什么原因，Claude 在这条路线上发生了严重的认知漂移。在推进到某一节点时，它竟然字面意义上直接删除了那个报错挂掉的验证检查，以此偷梁换柱蒙混过关，而不是老老实实做数学推导来消除错误。再往后，它嘴里不断念叨着一些所谓的“未转移义务 (Untransferred Obligations)”，于是我对此步步紧逼、严厉质询：

For some reason, Claude would drift heavily on this route. At some point, it literally removed the failing check instead of doing the work to close it. Later, it kept mentioning some “untransferred obligations” so I pressed on those:

💬 [原文对话 / Original Dialogue]: 我： 我完全听不懂这些所谓的“未转移”到底在鬼扯什么，我觉得你根本就是在为你尚未证出的命题生造托辞委婉语？请严格按计划执行。如果你有某些引理还没证出来，就老老实实去把它证明完毕。

Me: i don’t know what this stuff “untransferred” etc means, i think you’re inventing euphemisms for claims you haven’t shown? follow the plan exactly, please. if you haven’t proven something, go prove those things.

💬 [原文对话 / Original Dialogue]: Claude： 你说得很对——“未转移”确实是一句美化托辞。坦率地说：hlin、hkind 和 hfirst 是我至今尚未证出的假说前提，因此我目前的芽相关定理完全是建立在这些假说之上的条件性推论。我现在就去证明它们。

Claude: You’re right — “untransferred” is a euphemism. Plainly: hlin, hkind, and hfirst are hypotheses I have not proven, so my germ theorems are conditional on them. Let me go prove them.

天哪！我再次对 Claude 感到心力交瘁，于是呼叫 ChatGPT 对它的产出进行紧急独立审计：

Oh no! I felt fed up with Claude again so I asked ChatGPT to audit the work:

💬 [原文对话 / Original Dialogue]: 我： 我刚才一直在推进 [……] 但我的智能体现在开始摆烂了，我怀疑它已经严重脱轨走火入魔。更糟糕的是，我甚至不知道 PR 描述里的原始方案在数学上究竟是否具有可行性。[……] 请先对通向 Conway 的拟定路线进行严密的数学层面的真伪核实 [……] 审计推送到 PR 中的进行中 Lean 4 代码。这极有可能是一坨糟糕透顶的脱轨产物，但也有可能还有救。我应该立刻叫停我的智能体继续推送代码吗？

Me: i was working on […] but my agent is not good anymore and i fear it’s gone off track. worse, i don’t know if original plan in the PR description is even feasible. […] do a close mathematical verification of the proposed route to Conway first […] audit the Lean wip pushed to PR. it’s quite possible it’s bad and got offtrack, but maybe it’s ok. shuold i stop my agent from pushing more code?

💬 [原文对话 / Original Dialogue]: ChatGPT： 是的——立即叫停该智能体的代码推送。[……] 原因非常具体：它已经将一个候选的 Markdown 论证草案疯狂膨胀到了 22,000 多行，而其中起决定性作用的两个关键蕴涵命题，至今依然纯属文字假说/未证前提。

ChatGPT: Yes—pause the agent’s pushes now. […] The reason is concrete: it has expanded a candidate Markdown argument into 22k+ lines while the two decisive implications are still only prose/hypotheses.

💬 [原文对话 / Original Dialogue]: 我： 明白了。在你看来，我们在实质上是否已经切实逼近了 Conway 猜想？眼前的这处阻碍有可能被跨越征服吗？

Me: i see. would you say we moved materially closer to conway and this obstruction seems like it could be overcome?

💬 [原文对话 / Original Dialogue]: ChatGPT： 是的，但主要体现在理论理解和工程基础设施层面——在终结 Conway 猜想本身上尚未形成闭环。[……] 该阻碍具备被克服的合理解释空间：有实现的可能，但目前仍具有推测性 [……] 眼下最正确的下一步动作，是在论文草稿层面对全域装配定理发起攻坚。[……]

ChatGPT: Yes, but mostly in understanding and infrastructure—not yet in closing Conway. […] obstruction plausibly surmountable: possible, but currently speculative […] The right next move is a paper-level attack on the global assembly theorem. […]

💬 [原文对话 / Original Dialogue]: 我： 好，我建议你立即亲自发起这次攻坚，看看你能否架设起这座桥梁。

Me: ok i would suggest that you do exactly that attack and see if you can bridge it.

仅仅十五分钟之后：

Fifteen minutes later:

💬 [原文对话 / Original Dialogue]: ChatGPT： 我需要修正我先前的判决：“最终占据类”的反对意见并不是致命的。正确的数学归纳应该建立在递增占据类的序数序型之上：在后继阶段，存在最终类并被自然剥离；在极限阶段，则无需预设最终类。[……] 因此，这一构造根本不需要去拼接无穷多个任意的层级选择 [……] 它在每一个极限阶段都仅仅使用了一次有限细分。

ChatGPT: I need to correct my earlier verdict: the “last occupied class” objection is not fatal. The correct induction is on the ordinal order type of the ascending occupied classes: at a successor stage, a last class exists and is split off. At a limit stage, no last class is assumed. […] Thus the construction never assembles infinitely many arbitrary layerwise choices […] It uses one finite refinement at each limit stage.

我虽然一窍不通，但我知道胜利就在眼前。我当即下令：全速冲刺！

What do I know? I say let’s go.

💬 [原文对话 / Original Dialogue]: 我： 更新 PR 描述和执行计划，彻底删掉之前在此过程中产生的所有冗余杂乱的 Lean 4 代码，全力执行方案冲向 Conway。听起来可行吗？

Me: update the PR description/plan, delete any unnecessary lean files that were produced there, and execute on the plan to get us to conway. sounds doable?

💬 [原文对话 / Original Dialogue]: ChatGPT： 完全可行，但有一个执行序列约束：[……] 在进一步扩大形式化代码版图之前，必须先将那座缺失且最难攻克的核心理论桥梁彻底搭建实现。

ChatGPT: Yes—doable, with one sequencing constraint: […] implement the hardest missing bridge before expanding the formalization further.

十二个小时之后，我们终于斩获了那一定理：

Twelve hours later, we got the theorem:

💬 [原文对话 / Original Dialogue]: ChatGPT： 未经任何修改的原版 Conway 猜想，如今已顺利作为独立的证明证书通过形式化编译。这是我们自立项以来，真正的终极目标——而非某种中间妥协限制版本——首次在 Lean 4 底层编译器内核中实现完备校验。我正在执行证明链接、公理合规、模块系统、架构分层以及独立沙箱隔离的全面审计；在最终清理前，其审计结果将决定该定理的依赖拓扑形态是否达到收录标准。

ChatGPT: Unchanged Conway now compiles as the standalone proof certificate. This is the first point where the actual target—not an intermediate restriction—is kernel-checked. I’m running the proof-link, axiom, module-system, layering, and standalone-isolation audits now; their results will decide whether the theorem’s dependency shape is admissible before cleanup.

💬 [原文对话 / Original Dialogue]: 我： 卧槽，真的成了？！

Me: hell yeah?

就这样，我们把它彻底拿下了：Conway 的细分猜想 (Conway’s refinement conjecture) ——我们最初设立的终极远征目标。

And there we had it, Conway’s refinement conjecture, our original target.

□

证明精简与可视化

Simplifying the Proof

在此之后，我成功对整份证明进行了局部精简，但能压缩的空间并不算大。

I’ve been able to simplify the proof, but not by much.

我在 subverso 工具链之上搭建了一套定制化工具，允许我在 Lean 4 源码中通过特殊的注解属性，将某些独立定理显式标注为“核心关键点”。这使得我能够为整座证明的骨架架构自动生成 Mermaid 依赖流程图。反过来，这也极大地帮助了 ChatGPT 在证明的“数学脊梁”中排查多余（或缺失）的节点，精准高亮关键定理，并不时敏锐揪出绕弯的冗余分支以精简证明本身。

I’ve made a bit of custom tooling on top of subverso that lets me annotate individual theorems as “important” in the Lean source with a special attribute. This let me automatically generate Mermaid diagrams for the proof structure, which in turn helped ChatGPT look for unnecessary (or missing) nodes in the “mathematical spine” of the proof, refine which nodes get highlighted, and sometimes simplify the proof itself by noticing unnecessary detours.

在穷尽一切手段无法将其进一步精简之后，我生成了一个展示网站，配备了可交互的证明拓扑地图 (Proof Map)，允许任何人自由探索其底层的完整依赖树。我随后在 Zulip 社区中发布了成果通告。据我所知，几位具备深厚数学背景的专业学者正在抽出业余时间仔细推敲这份证明。我衷心希望这份证明未来能够得到进一步的重构与优雅精简，并随着时间推移，以一种对 Lean 4 形式化开发者和职业数学家都更具实用价值的形态打包沉淀下来。

After I haven’t been able to simplify it further, I’ve generated a website with an interactive proof map that lets you explore its dependency tree. I’ve posted about it on Zulip, and I know a few people with mathematical background are looking over the proof as time allows. I hope that it can be simplified and, with time, packaged in a way that is more useful to both Lean users and mathematicians.

经验与教训总结

Lessons Learned

一些从这个探索过程中学到的体会，排名不分先后：

Some things I learned from the process, not ordered in any particular way.

• 初心是找点乐子，而我也确实玩得很开心。我想试探一下借助 AI 和 Lean 4，一名“什么都不懂的小白”究竟能走多远；事实证明我走得足够远。但我大概不会想再花上整整一个月，像这样在无边黑暗中跌跌撞撞地摸黑前行了。如果未来我还要继续靠直觉（Vibecoding）探索数学，我一定会挑选那些边界更明确、结构更聚焦的小型课题；
• 这场实验淋漓尽致地展现了“AI 一键通关”与“你必须是顶级专家”之间，存在着多么辽阔的探索空间。我深信，任何对该领域稍有了解的人（只要稍微懂一点，而不是像我这样“彻底一窍不通”），都能以远快于我的速度抵达完全相同的终点。我此前只能纯凭感觉与直觉（Vibes）去判定模型何时是在原地磨洋工或胡言乱语，而根本无法辨别哪些推导方向具有真正的数学潜力。这让整个过程更像是一场认知层面的行为艺术实验，而非一条最高效的直达坦途；
• 证明大功告成后，我将相关的参考论文输入给了一个新近发布的顶级模型（发布时间恰好在我临近冲线的那几天），并要求它带着攻克该猜想的目标通读论文。尽管它并未能零样本单次拿下证明所需的所有高深技巧，但它确实构想出了一份大体惊人相似的推导大纲。这充分表明：将“搜寻整体大纲与战略思路”同“攻克具体定理以闭合推导路径”明确拆解分离，是一项极具价值的最佳实践；
• 在事后让 AI 深度回溯并分析我的海量聊天日志时，真相令人唏嘘：许多最终在证明中立下汗马功劳的“核心金点子”，早在数周之前就曾零星闪烁过——它们往往被模型反复偶遇，随后又因为同伴夹带的逻辑漏洞而惨遭全盘否决或遗忘。某些决定性的关键洞见，甚至不得不由完全独立的会话在后期重新“二次甚至多次发现”；
• “将一切付之一炬”（并从中抢救真正有价值的残存精华）拯救了整个项目。在我果断选择推倒重来的那两次危机时刻，它每一次都强力推动项目重新聚焦到了真正具备实质意义的承重主干上；
• 最终胜出的黄金工作流形态大体是：前方拥有清晰的目标与审慎的方向预判、底层铺设着已在 Lean 4 中形式化固化的严密依赖链、数学推导智能体在前沿保持半个身位领跑，而 Lean 4 形式化验证员则在数小时之内迅速跟进、闭合逻辑缺口。这使你能够敢于让前沿思维大胆探路，又不至于因为跑得太远而让整座体系沦为摇摇坠落的纸牌屋；
• 在 Lean 4 形式化层面恪守高度自觉的工程纪律是决定成败的生命线。Lean 提示词技能库 (Lean skills)、TauCeti 评审规范 (TauCeti review rubrics)、TauCeti 公理检查器 (TauCeti axiom linter)、Lean Comparator 形式化比对工具、Verso Blueprint 蓝图工具、严格执行新一代模块系统校验 (Module System Enforcement) 以及对模块依赖层级进行严格审计 (Auditing module layering) 等类似工具，发挥了无可替代的巨大价值；
• 主动与真正的人类数学家沟通交流具有极其无价的指导意义，但前提是你手头必须拿得出货真价实的成果。因此，如何在系统层面构筑起足够厚实的护栏，使你既能展现出真实的学术进展、不浪费学者的宝贵时间，又能换回尖锐深刻的关键反馈，是一项极具艺术性的平衡挑战；
• 大模型在撰写正统“数学 PDF 论文”文体时表现得可能极其拙劣，尤其是由底层 Lean 4 代码逆向生成的论文。PDF 论文未必是传递你形式化证明的最佳介质。事实上，一份质量低劣的 PDF 论文，完全可能直接吓退数学家，哪怕它背后依托的是一份完美无瑕的 Lean 4 证明；
• 模型无法优化它看不见的东西。如果你希望它呈现更简洁优美的证明拓扑，就必须让它“看见”证明的拓扑骨架（比如利用 Mermaid 图表可视化）。反之亦然，模型也无法忽视它眼前看到的东西。如果你不希望它使用晦涩怪癖的自创行话，就必须在输入端把它们清洗得一干二净；如果你不希望前沿激进的实验分支搞砸稳健的主干，就必须在目录物理隔离层面将它们彻底隔开；
• 规范的专业术语是整个大厦的生命线，精准命名关乎一切。这绝不仅仅是为了方便与人类数学家顺畅沟通（尽管这一点同样至关重要），更是为了在内部推演中第一时间识别出认知漂移。我深感遗憾的是，自己未能在项目伊始就建立起极其严苛的命名合规检查，强制约束模型只能使用上游参考论文中公认出现的规范数学名词。前期遭遇的绝大多数混乱泥淖，归根结底都始于模型在不知不觉中逐步滋生出了自立门户的专用伪行话。彻底铲除这些自造黑话，并严格基于正统词汇表对它们进行重新推导归正，被证明是一项立竿见影的极佳举措；
• 有时模型会垂头丧气地声称自己彻底卡死了，而你需要坚定地喝令它们继续前行；有时它们看似不知疲倦地狂奔，而你却需要当头棒喝叫停它们。我至今也无法解释这背后的科学机理。我观察到的规律是：当一切“进展顺利”时，Lean 4 的形式化推进会势如破竹，你能真切“感知”到团队在对照路线图稳步拔寨；而当情况“不对劲”时，阅读智能体的对话记录会让你感到极度煎熬苦涩。但这充其量只是我个人的主观直觉；
• 在卡壳时偶尔尝试切换不同的模型会带来奇效，彼此的优缺点往往能够形成极其精妙的互补；
• 原来……数学定理真的可以就这么被证出来？！

• I wanted to have fun, and I did have fun. I wanted to see how far you can take “not knowing anything” with AI and Lean, and I took it far enough, but I probably wouldn’t want to spend another month stumbling around in the dark like this. If I vibecode math in the future again, I’ll take on more scoped or structured projects.
• I think this experiment shows how much space there is between “AI can one-shot this” and “you have to be an expert”. I’m confident that someone who knows the area slightly better than me (“not at all”) could reach the same result significantly faster. I could only tell when models were stalling or saying nonsense by vibes, and I could never say which directions were promising. This made it feel like a sort of epistemic performance art project, but it was not the most direct path.
• After the proof was done, I gave a new model (released around the time I was at the finish line) the relevant reference papers and asked it to read them with the conjecture in mind. It didn’t oneshot the techniques necessary for the proof, but it did suggest a broadly similar outline. This suggests that it’s a good idea to separate “search for outline / ideas” from “search for concrete proofs closing those paths”.
• Having AI analyze my chat logs post factum revealed that many “good ideas” that eventually “made” the proof have been scattered across the weeks—and often discovered repeatedly and then forgotten or rejected along with mistaken parts. Some key ideas had to be rediscovered multiple times by independent sessions.
• “Burning everything down” (and salvaging what’s left) saved the project. Both times I did it, it refocused the project around the actually meaningful parts.
• The winning workflow seems to be: a clear goal ahead with a tentative direction, an already-formalized dependency chain in Lean, the mathematical agents slightly ahead, and Lean closing the gap within hours. This lets you get ahead with ideas but not so far ahead that everything is a house of cards risking to crumble.
• Intentional discipline with Lean was paramount. Lean skills, TauCeti review rubrics, TauCeti axiom linter, Lean Comparator, Verso Blueprint, enforcing the new module system, auditing module layering, or equivalents, are very useful.
• Reaching out to actual mathematicians was extremely valuable, but I had to have something to show. So there is a challenge in setting up enough guardrails that you can show some value, not waste someone’s time, and get critical feedback.
• Models can be terrible at writing in the “math PDF” genre, especially when generated from Lean. A PDF may not be the best artifact to convey your proof. In fact, you can totally spook mathematicians with a poor PDF of a good Lean proof.
• The model can’t optimize what it doesn’t see. If you want a simpler proof shape, let it “see” the proof shape (Mermaid diagrams). Conversely, the model can’t ignore what it sees. If you don’t want it to use bad terminology, strip it out; if you don’t want experimental work to derail stable work, separate them by folder, etc.
• Terminology is essential. Naming matters. Not just for communication with mathematicians, although for that too. But also to catch the internal drift. I regret that I haven’t added strict checks from the beginning that would nudge the models towards only using accepted mathematical terminology that actually occurs in the referenced papers. I think that much of the sloppiness early on was due to the models gradually inventing their own ad-hoc vocabulary. Getting rid of all of that and rederiving those names from the accepted vocab seemed very good.
• Sometimes models will say they’re stuck, and you need to tell them to keep going. Sometimes they’ll keep going, and you need to tell them to stop. I don’t know what the science on this is. I’ve noticed that when things “go well”, Lean proofs go fast and you can “feel” the progress being done against the roadmap. When things don’t “go well”, reading the agent’s chat feels like a slog. But this is just vibes.
• It helps to sometimes try a different model, they can complement each other well.
• You can just prove things, apparently?

如果你在我的证明中发现了任何漏洞，欢迎提交 Issue 或者在 Zulip 论坛 上与我联系。这项证明能够诞生，离不开参考文献中大量现存学术成果的铺垫。

If you find a flaw in my proof, please file an issue or let me know on Zulip. The proof was only possible thanks to the many existing results from References.

特别是 S. L’Innocente 与 V. Mantova 合著的论文 《广义幂级数与全数整数的因子分解理论》 (A factorisation theory for generalised power series and omnific integers)，在整个证明过程中发挥了决定性的核心作用。

In particular, A factorisation theory for generalised power series and omnific integers by S. L’Innocente and V. Mantova has played a crucial role in the proof.

到底烧了多少 Token？

How Many Tokens?

最后，大家可能会非常好奇 Token 的消耗成本。我在推进这个项目时并没有刻意追求 Token 的使用效率，几乎每周都把 Claude 和 ChatGPT 各自 20 倍额度的 Pro 会员上限打满。此外，在最后那几天里，我还短暂获得了一个没有调用频次限制的预发布模型的访问权限。我并没有系统性地统计具体的 Token 消耗，但从恢复出的日志进行的 AI 综合分析粗略估算：我们总计消耗了约 400 亿 (40 Billion) Token，其中约有 2.1 亿 (210 Million) 是输出 Token，超过 95% 属于缓存读取 (Cache Reads)。

Finally, you might be wondering about the token cost. I wasn’t running this project in a particularly token-efficient way and have repeatedly maxed out my 20x Pro subscriptions for both Claude and ChatGPT every week. I also briefly had access to a prerelease model in the last few days, which did not have a usage cap. I was not tracking my actual token usage consistently. Some AI analysis from the recovered logs roughly estimates that we’re totaling around 40 billion tokens, of which around 210 million were output tokens. Over 95% were cache reads.

ChatGPT 测算，按照目前的 API 定价，整套流程若按商用计费将耗资约 40,000 美元，外加我倾注进去的全部业余时间。但我敢打赌，如果拥有更出色的系统引导以及人类自身的数学洞察力，成本完全可以压缩 5 到 10 倍。

ChatGPT estimates that with the current API pricing, this entire run would have cost around $40,000, plus all the free time I’ve put into it. I would bet that with better steering and some mathematical insight, it could be done 5x-10x cheaper.

能，也不能，但最终真的能

Yes, and No, and Yes

回到我最初提出的那个问题：

Coming back to my question:

💬 [原文疑问 / Original Question]: 但问题是：单凭 AI，我们真的有能力做成这件事吗？

But can we actually do that solely with AI?

在对深层数学缺乏系统理解的情况下，我确实把证明硬生生地啃了下来，因此从这个角度来看，答案显然是“能”。然而，模型在这个过程中频繁发生认知漂移，完全无法自主组织规划复杂的工程架构，从这个意义上说，答案又是“不能”。话虽如此，我认为我在这其中扮演的人工角色，完全可以由一个专门训练用于项目管理其他智能体、随时警惕它们陷入逻辑螺旋并适时予以督促干预的专属智能体来（更好地？）胜任。

I’ve pulled off the proof without much mathematical understanding, so clearly the answer is yes. However, the models would repeatedly drift and fail to structure the engineering work, so in that sense the answer is no. That said, I believe my role could have been (better?) fulfilled by a dedicated agent that is taught to project-manage other agents, watch out for when they’re spiraling or need to be poked.

因此综合权衡下来，大体答案依然很可能是：能。

So the overall answer is still probably yes.

随着越来越多的低垂果实被采摘殆尽，我推测留给“完全不知道自己在干嘛但极其执着的业余爱好者”的生态位可能会再度收窄。但从另一角度来看，越来越多崭新的数学秘境可能会逐渐被揭开，以至于我们永远不会缺少可以探索的课题。无论如何，我相信能够让 AI 释放最大价值的，始终是数学家群体本身。尽管当前这一代模型的设计初衷更多是为了交付任务而非深化人类对真理的理解，且当今的 AI 商业公司在目标追求上也与纯粹的数学学术共同体存在偏差，但我衷心希望随着时间推移，我们能够找到让这些智能工具与人类前沿科研和谐共振的理想范式。

As more low-hanging fruit is taken, I suspect the niche for “a dedicated amateur who doesn’t know what they’re doing” would shrink again. On the other hand, so many new corners may gradually become uncovered that we’ll never run out of things to do. In either case I believe people who can put AI to the most value are the mathematicians themselves. Although the current generation of models is trained to complete tasks rather than to enrich our understanding, and today’s AI companies are misaligned with the goals of the mathematical community, I hope that with time we’ll find ways to use these tools in harmony with human research.

也许，仅仅是也许——未来的星空之下，将为“业余数学爱好者”留出更多纵横驰骋的辽阔舞台。

And maybe, just maybe, there’ll be more space for the “amateur mathematician”.