想象一下：你打开 Mac 桌面上一个叫 Star Fleet Math 的应用，点击「开始」。一瞬间，20 个 Codex Agent 同时启动，每个运行在独立的 60 核 vCPU 服务器上，各自盯着一道悬而未决的数学难题。它们有的在搜索 arXiv 论文，有的在生成 Lean 4 证明代码，有的在调用 SAT/SMT 求解器暴力验证。

这不是科幻小说。这是 Colin Snyder 刚刚发布的真实项目。他用 20 个并行 Codex 账户，向 Erdős 数学问题发起了前所未有的「群狼战术」式冲击。

发生了什么？#

Star Fleet Math 是一个 Mac 桌面应用，底层控制着 20 个自定义的 Agent「星际飞船」（starships）。每个飞船运行独立的 GPT-5.6 实例，配备 60 核 vCPU、120GB 内存的沙箱环境，以及完整的数学工具链：

  • 定理证明器：Lean 4，所有解答必须经过形式化验证
  • SAT/SMT 求解器：CaDiCaL、kissat、Z3，用于搜索和验证
  • 计算机代数系统：SageMath、PARI/GP、GAP、Macaulay2
  • 向量检索：基于 Gemini Embeddings + Chroma 的 Lean 4 定理库，支持英文自然语言搜索
  • 论文检索：Firecrawl 索引的 arXiv 论文和 GitHub 仓库
  • 长时记忆：名为 Ton 618 的依赖图谱系统，每个已证明的定理都织入图谱，让知识不断累积

这套系统对 650 个 Erdős 问题进行了测试，其中 27 个已经提出了解答。注意，这里是「提出解答」，不是「最终证明」。每个解答还要经过 Claude Fable API 包装的证明审核 Agent 审查，再由人类（Colin 本人）通过 iMessage 进行最终确认。

为什么这件事值得关注？#

1. 从「写代码」到「做研究」的跃迁#

过去我们谈论 Codex，场景通常是：重构代码、修 Bug、写测试、部署服务。这些都是「工程任务」。Star Fleet Math 把 Codex 推向了完全不同的领域：数学研究。

数学研究对 Agent 的要求远高于写 CRUD。它需要：

  • 理解抽象的定义和定理
  • 在庞大的搜索空间中寻找证明路径
  • 生成形式化的 Lean 4 代码（一门以严格著称的定理证明语言）
  • 在失败后调整策略，而非简单重试

这意味着 Agent 的能力边界正在从「执行已知方案」扩展到「探索未知领域」。

2. 并行 Agent 架构的实战验证#

20 个 Codex 并行运行不是简单的 & 符号叠加。这套系统的架构设计值得深入研究：

  • 独立沙箱：每个飞船有独立的 60 核 vCPU 和完整工具链，避免资源争抢
  • 共享知识库：Ton 618 依赖图谱让「已证明的定理」跨飞船复用
  • 分层审核：Claude Fable 初审 + 人类终审的双重验证机制
  • 弹性伸缩：CPU 可爆发至 2000 vCPU 用于大规模并行搜索，H100 GPU 用于深度学习推理

这种「独立执行 + 共享知识 + 分层审核」的模式，可能成为未来多 Agent 系统的标准范式。

3. Lean 4 作为 Agent 的「编译器」#

最精妙的设计是：所有解答必须通过 Lean 4 的形式化验证。Lean 4 不是 LLM，它不会「幻觉」。一段证明要么通过类型检查，要么不通过。

这相当于给 Agent 的输出加了一层数学级别的编译检查。在软件工程中，我们通过编译器、类型系统、单元测试来保证代码质量。在 AI 数学研究中，Lean 4 扮演了类似的角色。Codex 可以随意生成证明尝试，但只有通过 Lean 4 验证的才算数。

这意味着什么？#

Codex 不再是「编程助手」，而是「通用推理引擎」#

Star Fleet Math 的核心洞察是：Codex 本质上是一个推理引擎，编程只是它的一个应用场景。把它接入 Lean 4、SAT 求解器、arXiv 论文库之后，它就变成了数学研究工具。同理，接入法律条文库和判例检索，它可以是法律研究工具；接入医学文献和临床试验数据，它可以是药物研发助手。

多 Agent 协作的门槛正在降低#

Colin Snyder 是一个人完成这个项目的。用他自己的话说：「Everything is built from scratch in TypeScript & Bun」。一个开发者，用 TypeScript 和 Bun，搭建了 20 个 Agent 的并行系统。这说明多 Agent 架构的门槛已经没有想象中那么高，关键在于设计思路，而非团队规模。

开放问题的「工业化攻克」成为可能#

27 个 Erdős 问题提出解答，这个数字本身可能还不够惊艳（这些解答仍需数学界同行评审）。但重要的是范式：一个人，20 个 Agent，650 个问题同时开工。如果把这个数字放大到 200 个 Agent，甚至 2000 个呢？如果每个 Agent 不是运行几小时，而是持续运行几个月呢？

数学研究中那些「需要灵感」的开放问题，或许正面临着一场来自计算力的正面冲击。

局限与审慎#

需要冷静看待的是，Star Fleet Math 目前提出的是「解答提案」，而非「最终证明」。Erdős 问题的难度跨度极大，有些问题几行证明就能解决，有些则需要全新的数学工具。27 个提案中有多少能通过同行评审，还有待观察。

另外，系统的运行成本也不容忽视。20 个 60 核 vCPU 实例加上 H100 GPU 的并行计算，每天的云服务费用可能达到数千美元。这不是个人开发者能日常负担的规模。

展望#

Star Fleet Math 给我的最大启发是：AI Agent 的未来不在于「更聪明地对话」，而在于「更有效地行动」。Codex 强在它能操作文件系统、执行命令、调用 API，它是一个「行动者」而非「聊天者」。Star Fleet Math 把这种行动能力扩展到了数学研究领域，用 20 个并行 Agent 构建了一个小型的「AI 研究所」。

接下来值得关注的方向：

  • 多 Agent 之间的动态任务分配（目前是静态分配问题）
  • 跨 Agent 的实时知识同步（目前通过 Ton 618 图谱异步共享）
  • 成本优化（能否用更小的模型处理简单子任务？）

如果你也对 Agent 架构感兴趣，Star Fleet Math 的源码和技术细节值得深入研究。毕竟，亲眼看到一个开发者用 20 个 Codex 攻克数学难题，比读十篇 Agent 架构论文都更有说服力。

参考来源：Star Fleet Math — Solving Erdős Problems with Codex