用20个Codex账户并行解决20个埃尔德什难题

背景

Erdős 问题是由数学家 Paul Erdős 提出的系列未解难题，涉及数论、组合、图论等多个领域，许多问题附带奖金。传统上，这些问题依赖人类数学家的直觉与归纳技巧，但近年来，形式化证明系统和 AI 的进步为自动求解带来了新可能。Colin Snyder 及其团队在新图灵研究所（New Turing Institute）先前工作的基础上，构建了 Star Fleet——一个利用 Lean 4 形式化验证环境解决开放数学问题的 AI 系统。该系统同时运行 20 个并行的智能体（称为“starships”），每个智能体对应一个独立的 GPT-5.6 实例，部署在专用的 60-vCPU 服务器上，各自处理不同的 Erdős 问题。整个系统使用 TypeScript 和 Bun 从零构建，是运行在 macOS 桌面端的应用。

核心内容

系统能力

每个 starship 配备以下资源：

• CPU 与 GPU：支持 x86-64 CPU 突发至 2000 vCPU，用于可拆分为数千独立单核作业的搜索程序；H100 GPU 突发用于大规模并行搜索。
• 知识库：据作者所知最大的 Lean 4 前提（定理与引理）语料库，可通过 gemini-embeddings-2 和 chroma 向量数据库用自然语言检索；还包括通过 Firecrawl.dev 索引的 arXiv 论文和 GitHub 仓库。
• 验证与审查：基于 Claude Fable API 封装了证明验证智能体，用于审查提交的答案；在 Fable 批准后，通过 iMessage API 通知人类 Colin 进行二次审查。
• 长期记忆：Ton 618 本地长期记忆系统，将所有已验证的 Lean 4 前提（定理或引理）编织成依赖图，使证明可以累积复用。
• 计算沙箱：专用 60-vCPU、120 GiB 内存的沙箱，预装 SAT/SMT 求解器（CaDiCaL, kissat, Z3）、Google CP-SAT、计算机代数系统（SageMath, PARI/GP, GAP, Macaulay2）以及完整的 Rust、CUDA C++ 和 Lean 4 工具链。

解决方案：Erdős Problem #123

该问题（奖金 $250）属于数论：设 (a,b,c) 为两两互素的整数（均大于 1），问是否每个足够大的整数都可以表示为不同项 (a^i b^j c^k) 之和，且没有选中项能整除另一项。核心困难在于整除性条件——通常的凑数论证中，来自不同尺度的项容易形成整除关系，而若选择互不整除的项（即 antichain），则会因过于稀疏而无法覆盖连续整数。

早期尝试的局限

• 符号恒等式只能给出两个连续和，但每个残差类代表的跨度至少为模数减一，无法增长。
• 完全剩余系可解决同余，但无法控制数值跨度。
• Van der Waerden 和 Hales–Jewett 论证可构造任意长的初等项等差数列，但初始公差不可控，且基线随长度同步增长，无法得到归纳所需的乘法宽区间。

关键教训：仅靠加法宽度不够，还需定量控制下限端点。

同质指数坐标系

一个关键的简化是将问题限制在单一齐次指数层面：即只考虑指数和 (i+j+k = d) 的项。由于两两互素且指数为坐标比较，同一层面的不同单项式永远不会互相整除，自动满足 antichain 条件。于是问题转化为齐次层面上的子集和问题，而整除性约束自动消失。

边码构造

通过一种边码（edge-code）构造，可以在单一层面上得到具有不同模 (m) 余数且携带有限进位的本原子集和。利用 Mathlib 中 Hales–Jewett 定理得到的 Van der Waerden 论证，可进一步得到任意长的精确等差数列，每个元素都是该层面上的本原和。

将等差数列转化为大区间

将三个基数按大小排序，选择合适参数，构造两个互素的齐次平移权重。通过不同平移将多份等差数列放在不同的指数带上，使得所有项仍处于同一齐次层面。一个齐次进制引理表明，系数和可以覆盖宽度至少为 (W) 的完整区间。将系数替换为对应的等差数字集合，就得到了一个步长为 (d)（等差数列公差）的格点上的区间。

用面校正填充余数

接下来，在每个足够高的齐次层面上，针对任意模数 (m) 构造本原校正集，这些校正仅依赖于三个坐标面，且总大小受指数支配。将模数取为前一步的步长 (d)，校正集与等差数列的严格内部项不相交，且其跨度最终小于进制区间的宽度，因此余数粘合可以将格点区间转化为真实的连续整数区间，满足下界固定。

关键突破：可选内部壳层

尽管此时已得到连续区间，但其乘法宽度仍仅为常数，这正是之前基线问题的瓶颈。决定性思想是：在同一齐次层面上，利用尚未使用的单项式。对线性多个索引，选取恰好超出所有等差带的某个指数，并在剩余指数中取几何网格的最后一点，构造至少 (L) 个可选单项式，每个的大小都不超过已有区间宽度。这些可选单项式可以选择使用或不使用，从而扩展连续区间而不改变其下限端点。由于它们位于同一层面且超出了等差指数带，本原性和不相交性得以保持。它们的总贡献为 (L \cdot C)，而下限仍为 (R_{\text{low}})，因此区间长度与下限的比值随 (L) 增长，最终满足归纳所需的乘法宽区间，从而完成证明。

整个结果在 Lean 4 中被形式化为定理 Erdos123.erdos_123。

关键要点

• 系统同时使用 20 个独立的 GPT-5.6 实例（对应 20 个 Codex 账户）并行求解不同的 Erdős 问题，每个实例拥有专用服务器和沙箱环境。
• 利用 Lean 4 形式化证明系统确保答案的严格正确性，并通过 Claude Fable API 和人类专家进行双重验证。
• 通过将问题限制到齐次指数层面，自动满足“互不整除”条件，使原问题转化为纯加法子集和问题。
• 边码构造与 Hales–Jewett 定理结合，在单一层面上生成长等差数列，再通过进制引理和面校正扩大为连续整数区间。
• 关键创新在于“可选内部壳层”技巧，在不改变下界的前提下，利用同一层面上的未用单项式线性扩展区间宽度，从而满足归纳所需的乘法增长。
• 该解决方案针对 Erdős Problem #123（奖金 $250），属于数论领域，利用了大量现有数学库（Mathlib）和计算工具。

意义与影响

该工作展示了 AI 系统在解决经典开放数学问题上的潜力。通过并行部署多个高级语言模型实例，并集成形式化推理、大规模搜索和外部知识库，Star Fleet 成功攻克了一个长期未解的难题。其方法论具有可迁移性：同质坐标简化、差分粘合与可选壳层等思想可能适用于其他涉及整除性约束的加法组合问题。更重要的是，系统开源（基于 TypeScript/Bun）且模块化设计，未来可扩展到更多 Erdős 问题，甚至成为自动定理证明领域的通用框架。这次成功也验证了在计算资源充足时，AI 能够超越人类直觉的局部技巧，系统性构造出复杂的归纳结构，为 AI for Math 树立了新标杆。