我是如何“凭感觉”证明康威精炼猜想的

快速摘要

Dan Abramov 使用 Claude、ChatGPT 和 Codex 智能体生成、审计并用 Lean 形式化证明了全能整数（omnific integers）的康威精炼猜想；该证明通过了机械检查，但尚未经过独立验证。

---

康威猜想的内容

康威精炼猜想断言，对于任何全能整数（omnific integers）的乘积等式 (a b = c d)，都存在整数 (e,f,g,h) 使得：

• (a = e f)
• (b = g h)
• (c = e g)
• (d = f h)

换句话说，全能整数的任意两种因式分解都承认一个共同的精炼，这反映了初等整数的一个性质，即乘积可以分解为素因子并重新组合。

AI 驱动的研究流程

1. 问题选择

• Claude 被提示选择一个超现实数领域的开放问题。它选择了精炼猜想，并引用了 L’Innocente 和 Mantova 最近的工作，该工作将猜想简化为关于 (K((\mathbb{R}^{\le 0}))) 中不可约元的陈述。
• 作者指出，Claude 的简化并不完整，但由于该问题与 ONAG 出版 50 周年的情感联系，它仍然具有吸引力。

2. 早期的“一键式”尝试

• 最初的提示要求 Claude “做出突破”。模型生成了连贯性差、充满术语的散文，无法验证。
• 转向 ChatGPT（称为 Sol）后，虽然主张较为温和，但仍需要大量的人工审查。

3. 多智能体实验室 (Codex)

• 一个 项目经理 (PM) 智能体协调工作流。
• 两个 数学 智能体生成候选引理。
• 一个 红队 (Red) 智能体尝试寻找漏洞。
• 一个 随机 (Random) 智能体探索边缘想法。
• 一个 Lean 智能体将有希望的结果翻译成 Lean 代码。
• 智能体通过“自助餐厅”聊天室进行交流，在保持角色边界的同时实现交叉授粉。

4. Token 消耗与成本

• 总共处理了约 400 亿个 token，其中输出约 2.1 亿个。
• 预估 API 成本：≈ 40,000 美元。

关键里程碑

周次	里程碑	结果
1	问题框架与初步提示	Claude 生成了一个模糊的问题陈述；ChatGPT 提供了关键的“怀疑”声音。
2	使用 Codex 智能体建立实验室	生成了数十份草稿“论文”；许多包含发明的术语和逻辑漏洞。
3	第一次死胡同与失败的“引导”证明	ChatGPT 声称证明了完整结论，但新会话揭露了循环论证。
4	通过纠错进行基础验证	模型在同行评审的参考资料中发现的错误得到了作者的证实，增强了信心。
5	烧毁与挽救策略	丢弃了大部分嘈杂的草稿，保留了关于 Hahn 级数中 有限度素性 的连贯结果。
6	形式化验证	两个独立的 Lean 智能体认证了有限度结果，随后认证了完整的精炼猜想。
7	证明映射工具	自定义脚本生成了 Mermaid 图表和交互式 Web UI，以可视化依赖结构。

最终的 Lean 证明

• 证明位于 GitHub 仓库 gaearon/conway‑refinement 的 ConwayRefinement/Standalone 下。
• 每个独立文件仅导入 Mathlib，确保了陈述的自包含性。
• 审计验证：
  • 没有引入额外的公理。
  • 导入遵循独立策略。
  • 每个陈述都有配对的 Lean 证明。
• 由 Lean 内核编译的 证明证书 确认了猜想的陈述（参见编译视频）。

经验教训

1. 感觉 vs 理解 – 该项目在没有深厚个人专业知识的情况下成功了，但需要不断的“感觉检查”来检测偏差。
2. 智能体纪律 – 用于背景形式化和新结果的独立 Lean 智能体防止了稳定代码的污染。
3. 审计基础设施 – 独立文件夹、模块层级检查和公理检查器对于审稿人的信任至关重要。
4. 人类反馈 – 给数学家发送关于纠错的电子邮件提供了现实检验，并为可信度提供了立足点。
5. 模型互补性 – Claude 擅长结构化的 Lean 生成；ChatGPT 更擅长探索性数学和批评。
6. Token 经济学 – 更具引导性的工作流可以将成本降低 5–10 倍。
7. 证明呈现 – 将 Lean 代码翻译成可读的 PDF 仍然是一个瓶颈；交互式证明映射有助于弥合差距。

社区反应（精选 HN 评论）

“这种方法感觉就像巫术与魔法的区别；作者召唤了强大的存在（LLM），却并不完全理解咒语。” – @gbjcantab

“我不是数学家。‘在每个间隙中生成’规则是如何让你超越有理数的？” – @rlue

“该工作流反映了现实世界的工程过程：多智能体、对抗性测试和持续集成。” – @spongebobstoes

“证明令人印象深刻，但如果没有独立验证，数学界仍将保持怀疑。” – @patcon（链接到一位教授的评论）。

开放问题

• 验证 – 独立的数学家需要审计 Lean 代码并确认逻辑步骤。
• 简化 – 目前证明长度较大；未来的工作可能会使用生成的证明映射对其进行压缩。
• 泛化 – 同样的多智能体流水线能否在没有领域专业知识的情况下应用于其他开放问题？
• 模型对齐 – LLM 提供商如何更好地支持严谨的数学研究，而不鼓励“幻觉”定理？

---

作者欢迎对证明仓库和 Zulip 频道进行批评、错误报告和讨论。