使用 20 个并行运行的 Codex 帐户解决 20 个 Erdős 问题

27 Erdős 问题 0 前沿数学问题 0 千年问题 Star Fleet 是一个人工智能系统，使用 Lean 4 解决世界上最难的开放式数学问题。它是一个 Mac 桌面应用程序，可并行控制多达 20 个称为“星舰”的自定义代理线束，每个线束在专用的 60-vCPU 服务器上运行自己的 GPT-5.6 实例，并处理单独的数学问题。一切都是在 TypeScript 和 Bun 中从头开始构建的。每艘星舰都可以访问： x86-64 CPU 突发，最多 2,000 个 vCPU，用于搜索程序，可分割成数千个独立的单核作业 H100 GPU 突发，用于大规模并行搜索程序 世界上最大的精益 4 前提语料库（定理和引理），可通过 gemini-embeddings-2 和色度向量 db 以简单英语搜索 Firecrawl.dev 索引arXiv.org 研究论文和 GitHub 存储库 Claude Fable API 封装在证明验证器代理工具中，用于审查提交的答案 + iMessage API 在 Fable 批准后要求 Colin（人类）进行额外审查 Ton 618，一个本地长期记忆系统，其中每个经过验证的精益 4 前提（定理或引理）都被编织成依赖图，因此证明复合 专用的 60-vCPU、120 GiB 内存沙箱预装了 SAT/SMT 求解器（CaDiCaL、kissat、Z3）、Google 的 CP-SAT、计算机代数系统（SageMath、PARI/GP、GAP、Macaulay2）以及完整的 Rust、CUDA C++ 和 Lean 4 工具链 所有 650 个 Erdős 问题 630 前沿数学 14 千年问题 6 提出的解决方案 ( 27 ) 列出的许多问题“开放”包含已经在线提供的非正式或部分答案；我们非常努力地避免解决任何此类问题。 1 ) Erdős Problem #123 Erdős Problem www.erdosproblems.com/123 › 问题 设 a , b , c ≥ 1 a,b,c\geq 1 a , b , c ≥ 1 是三个成对互质的整数。是否每个大整数都是 a k b l c m a^kb^lc^m a k b l cm ( k , l , m ≥ 0 k,l,m\geq 0 k , l , m ≥ 0 ) 形式的不同整数之和，其中没有一个可以整除任何其他整数？ （Erdős 问题 #123 — 奖品：250 美元 — 数论 — https://www.erdosproblems.com/123） › 结果 对于每个整数 a,b,c>1 的成对互质三元组，每个足够大的整数都是不同项 a^i b^j c^k 的和，使得没有选定的项能整除另一个项。在精益中，这是定理 Erdos123.erdos_123 ：Erdos123.IntishedStatement。 def IntendedStatement : Prop := ∀ a b c : ℕ, 1 < a → 1 < b → 1 < c → PairwiseCoprime3 a b c → IsDComplete (Smooth3 a b c) /-- Erdős 问题 123，针对预期的非简并假设 `a,b,c>1`。 -/ 定理 erdos_123 : IntendedStatement := returned_erdos_123 › 解决 Erdős 问题 123 的报告 该问题及其为何抵制通常的归纳法 对于成对互质整数 a , b , c > 1 a,b,c>1 a , b , c > 1 ，考虑数字 a i b j ck ( i , j , k ≥ 0 ) 。 a^i b^j c^k \qquad (i,j,k\ge 0)。 a i b j c k ( i , j , k ≥ 0 ) 。该问题询问是否每个足够大的整数都是不同的此类数字的总和，并附加要求没有选定的被加数可以整除另一个 。可分性条件才是困难的真正根源。普通的完整性论证可以使用不同尺度的许多术语，但不同尺度的术语往往通过整除性进行比较。相反，选择作为可整性反链的集合在算术上可能过于稀疏而无法填充连续的整数。早期的工作已经开发出一种强大的简化方案：选择所需的余数以一个基数为模的校正，减去它，除以该基数，然后归纳。对于特定的三元组，经过有限的计算机检查后会成功。然而，一般来说，它留下了一个顽固的有限种子问题：必须首先表示乘法宽区间 [ N , CN ] [N,CN] [ N , CN ] 中的每个整数。校正归纳并不构造该区间；它只是传播它。这解释了为什么几个有吸引力的部分想法没有解决这个问题：差一的有符号恒等式给出两个连续的和，但每个类的一个留数代表必然至少扩展了模数减一。在普通的残胶粘合下，宽度一间隔不能增长。完整的留数系统在原始水平上解决了同余问题，但没有提及它们的数值分布。范德瓦尔登和黑尔斯-朱厄特的论证产生了任意长的原始和的算术级数，但最初具有不受控制的公差。即使在修复公差之后，级数 B 0 + r d B_0+r d B 0 ​ + r d 也带有较大的正基线 B 0 B_0 B 0 ​ 。复制此类级数会以相同的速率增加宽度和基线，因此不需要产生归纳所需的乘法宽度种子。重要的教训是大的附加宽度是不够的。下限终点必须保持在定量控制之下。齐次级坐标系 第一个结构简化是在一个齐次指数级 i + j + k = D 上进行。 i+j+k=D。 i + j + k = D 。 F