我是如何通过 AI 和 Lean “直觉”出康威精炼猜想的证明的

TL;DR

我构建了一个多智能体 AI 实验室，经过数月的提示词工程、高 Token 消耗的实验以及 Lean 形式化验证，最终生成了一个经机器校验的康威（Conway）全能整数精炼猜想证明；该证明已通过 Palomar 注册表和非正式的专家评审，但尚未经过独立数学家的验证。

康威精炼猜想的内容

康威的猜想（1976 年）涉及全能整数（omnific integers），即超现实数树中的整数部分。它断言了一个精炼性质：如果对于全能整数 a,b,c,d 满足 ab = cd，那么必然存在全能整数 e,f,g,h 使得

[ a = ef,\quad b = gh,\quad c = eg,\quad d = fh. ]

在普通整数中，这是显而易见的（例如 210 = 10·21 = 6·35 可以精炼为 2·5·3·7）。该猜想探讨的是，这种因子重组性质是否同样适用于更丰富的全能整数，其中包括无穷大和无穷小值，如 ω, 2ω, ω^ω，甚至像 -ω/7 这样的“整体”无穷小。

AI 驱动的工作流程概述

该项目分为五个周期的阶段，每个阶段都在优化智能体、其角色以及与 Lean 的交互。

1. 第一周 – 天真的单次尝试

  • 提示 Claude 对该猜想进行“突破”。
  • Claude 生成了冗长、充满术语且逻辑不连贯、无法验证的文字。
  • 切换到 ChatGPT 的“怀疑论者”人格后，产生了一些简短、合理的引理，但仍未形成连贯的证明。

2. 第二周 – 多智能体实验室

  • 在本地下载 Codex 以实现确定性的 Token 使用。
  • 设定具有明确角色的智能体：PM（项目经理）、Math（创意生成）、Red（对抗性审查）、Random（探索性）和 Lean（形式化）。
  • 智能体通过共享的“食堂”频道进行沟通；PM 负责协调合并。
  • 该工作流程产生了大量的 TeX 文档，但没有产生经过验证的新结果。

3. 第三周 – 死胡同与 Token 耗尽

  • 重新引入 Claude 进行 Lean 形式化；模型在证明和推翻自己的结论之间反复横跳。
  • TeX 堆栈增长到约 30 篇“论文”；任何单一错误都可能导致整个大厦倾覆。
  • 出现了一个看起来很有希望的全局证明，但审计发现存在循环依赖，证实了目前尚不存在证明。

4. 第四周 – 回归现实

  • 将重点转向验证同行评审文献（L’Innocente–Mantova 2024）中的具体错误。与作者确认了几个排版错误，建立了对模型发现实际问题能力的信任。
  • 销毁了之前所有的语料库，并要求 ChatGPT 挽救任何数学上合理的内容。
  • 在文献中发现了一个有限度素性（finite-degree primality）结果，经核实，这是一个新颖的定理。

5. 第五周 – 整合与最终证明

  • 构建了第二个独立的 Lean 智能体来认证该新颖结果，而第一个 Lean 智能体仅处理已建立的文献。
  • 引入了严格的独立文件夹（无内部导入）以及针对额外公理、模块分层和证明规模的自动化审计。
  • 生成了证明映射（Mermaid 图表）以可视化依赖关系，使模型能够修剪不必要的分支。
  • 经过多次“尽情发挥”的提示后，智能体生成了一个独立的 Lean 证书，涵盖了完整的精炼猜想，且编译时未添加额外公理。

关键技术产物

产物 描述
GitHub 仓库 – gaearon/conway-refinement 包含 Lean 源码、TeX 草稿和工具脚本。
Palomar 注册条目 – PALOMAR-2026-09-03-000002 机器验证，确认 Lean 内核接受了该证明。
独立文件夹 仅导入 Mathlib 的文件，确保每份人类可读的陈述不超过 500 行。
证明映射网站 – gaearon.github.io/conway-refinement 证明依赖树的交互式 Mermaid 图表。
自定义工具 – subverso 属性标注器、模块系统检查器和 Lean 比较器集成 强制执行清晰的模块分层并防止隐藏公理。

经验教训（结论先行）

  • AI 可以在作者不懂数学的情况下生成深度开放问题的机器验证证明，但工作流程需要严格的工程护栏、对抗性审计和频繁的“推倒重来”循环。
  • ChatGPT 在探索性数学方面比 Claude 更有效，而 Claude 在给定具体目标时，在确定性 Lean 代码生成方面表现出色。
  • 为已建立的文献和推测性结果分离 Lean 流水线可以防止污染，并使审计变得可控。
  • 人类对低级错误（如源论文中的排版错误）的验证建立了对模型输出的信心，并为协作提供了立足点。
  • 证明映射可视化和严格的模块隔离显著提高了模型的可解释性，允许智能体修剪“胡言乱语”的分支。
  • Token 成本巨大 – 整个运行过程消耗了约 400 亿 Token（约 4 万美元）；更好的引导可以将此成本降低 5 到 10 倍。

代表性社区反馈

“这个过程感觉像是一个行为艺术项目，作者从未真正学会数学，但模型完成了繁重的工作。” – m-steffen, HN 评论

“ChatGPT 的怀疑论者人格比 Claude 宏大的单次尝试要高效得多。” – nphardon, HN 评论

“证明映射和 Mermaid 图表帮助模型看到了证明的结构，并建议了简化方案。” – 作者本人的观察

待解决问题与后续步骤

  1. 独立数学评审 – 该证明尚未经过超现实数领域专家的审查；社区验证至关重要。
  2. 简化 – 目前的 Lean 代码包含许多辅助引理；更简短、更概念化的证明将有助于被接受。
  3. 泛化 – 该工作流程可应用于其他开放问题；目前正在准备一个模板仓库。
  4. 成本降低 – 开发更好的提示策略和 Token 高效的智能体将使大规模 AI 驱动的数学研究更易于实现。

最终总结

通过编排多个 LLM 智能体、强制执行严格的 Lean 形式化，并反复修剪幻觉数学，我成功生成了康威精炼猜想的机器校验证明。结果表明，即使对于远超作者专业知识的问题，AI 辅助定理证明也是可行的，但这也凸显了严谨的工程、对抗性审计和人类协作对于确保正确性和可信度的必要性。

Sources

相关