人月神话的逆向解 · 两个数学猜想，一套 Agent Swarm

Shaoyang Guo · 研究记录 · 个人主页

这篇文章回答一个问题：把两个开放数学猜想的攻坚工程交给一个分层组织的 agent swarm，结构怎么搭、任务的生命周期怎么管、一周能走到哪里？

两个猜想是两个完全独立的项目：Perelman 证明的 Lean 形式化住在 guoshaoyang-pku/lean-poincare，宇宙监督猜想住在 swarm-research/ai4math-swarm。它们各有各的仓库、各自的 DAG、队列和账本，互不共享任务；共享的只有一样东西——同一套 P0–P1–P2 控制面协议：顶层给方向，中层做计划，底层做执行。

这是一份工程日志：讲的是 swarm 的结构、任务的生命周期，以及两个项目在 2026-09-11 快照时刻的进度。数学结论以各仓库的验证器和审计账本为准，本文不替它们宣布任何东西。 文档范围声明

01发生了什么

系统不是从自动派工开始的，而是从人机讨论开始的。在 Perelman 项目里，我和主控 Astra 花了最开始的一段对话做同一件事：把“形式化 Perelman 证明”这个模糊目标，拆成数学上有依赖关系、工程上可以并行的若干方向；拆解的产物不是任务清单，而是一张逻辑 DAG 和五个研究组。宇宙监督项目里做的是同一件事的另一版：把猜想按场论设定切成互不泄漏的类，再给每类配上职能组长。

Perelman 项目之后的一周大致是四段：

三件事值得单独记住：执行力可以很快聚集；产出的严格部分全部经得起审计；而整套系统真正的产品，是一个把 years-long 数学工程拆成可执行、可恢复、可复核单元的控制结构。本文剩下的部分就在讲这个结构。

02两个项目，一套控制面

两个猜想必须分开跑，理由不是组织偏好，而是验证器不同：Perelman 项目的每一步最终要过 Lean kernel 和 axiom 审计；宇宙监督项目的每一步要过猜想类别的 schema 校验、一手文献核对和标定过的数值协议。验证器不同，任务卡的验收命令就不同，队列、账本和 ETA 也不能混在一张表里。所以是两个 repo、两条独立的任务流；共享的是角色协议、证据纪律和监督习惯。

下面三节讲共享的结构：三层角色、任务生命周期，然后分别看两个项目各自怎么分组。

03逆向的三层结构：P0 给方向，P1 做计划，P2 干活

“逆向”是相对于常见的 swarm 想法说的。常见的想法是正着来：把一个大任务均匀切碎，撒给一群同质的 agent，谁闲了谁领。我们反过来：先让少数“会看地图的”把问题变成方向，再把方向变成计划，最后才轮到大量执行。三层各司其职：

P0 · 人类主控 + Astra 主控

给出几个模糊方向，把项目分成几个小组。这是整套系统里唯一强制人机交互的环节：项目的拆解、方向的划分、边界的设定，都发生在 P0。主控不要求人类一次性写出所有定理——人类给出几个模糊方向、优先级和禁止越界的结论，主控负责把它们变成可审计的研究组，并冻结项目级 DAG 和证据规则。此后 P0 的工作是观察：各组的 checkpoint、blocker、ETA 和产物；不可逆的范围决策仍回到人类。

P1 · 组长（Astra 级）

每个组一个组长。接收方向之后，组长指定具体的 plan，把 plan 拆成带依赖和验收命令的任务，派发给 fleet，并且尽可能加速。组长最重要的权力是重排自己的局部 DAG：推进中经常发现原始接口的假设不正确、过强或缺少关键正则性，这时需要改路线，而不是让 worker 继续向错误方向堆代码。

P2 · DeepSeek Flash 舰队

做具体执行。每个 worker 在独立 worktree 里写 Lean 或研究产物，跑验证命令，写 checkpoint、heartbeat 和 result card；失败、传输中断或数学受阻时保留现场并暂停，而不是硬编一个假结果。

三层不是互相隔离的部门。P0 可以调整组的方向；P1 可以根据实际 blocker 重新规划局部路线；P2 的编译结果和失败原因又会反过来改变 P1 和 P0 的决策。两个项目都遵守同一条通信契约：组长向上只发六类消息——status、claim、artifact、blocker、direction_update、resource_request，每条都点名节点 ID、证据引用和下一个证伪者；主控向下发分配、预算变更、门禁与优先级调整。

一个必须说清楚的现实限制：协议允许 P1 使用 Astra 级模型，但已检查的远程主机目前实际配置的是 deepseek-flash。所以“Astra 级组长 + Flash 执行体”是当前架构的目标接口，已运行的队列仍主要由 DeepSeek Flash 驱动——模型名称不会因为主控用了 Astra 就被静默改写。 infra/swarm/leader_tasks.json · model_note

04任务生命周期：从 outbox 到 publication

结构回答了“谁做什么”，生命周期回答了“一个任务从生到死经过什么”。在 Perelman 项目里，这条链是写死在协议里的六个阶段，任何任务都不能跳段：

1. 计划与派发（P1）。组长是长生命周期任务，有自己的 worktree、checkpoint 和 comms/ 目录；子任务描述写在 comms/outbox/，必须带显式 ID、依赖、验收命令和命名 worktree，缺一不收。
2. 租约与调度（dispatcher）。dispatcher 只导入完备的任务卡，发租约、记账、负责恢复；依赖分两类——deps 要求前置任务通过验证，after_terminal 允许消费已结束但可能 blocked、paused 或 needs-review 的结果。
3. 隔离执行（P2）。worker 在独立 worktree 内工作，不碰别人的 worktree，也不碰 main；跑 lake build / lake env lean 或项目验证命令，持续写 checkpoint 与 heartbeat。
4. 结果卡（result card）。交付物必须是一张带产物路径和验证命令的卡，状态落在 verified / blocked / paused / needs-review 之一；没有卡就没有交付。
5. 门禁（gate）。编译 gate 给出 verified-by-compile；axiom gate 清点违禁公理；同时给结果打证据等级标签（proved / conditional / model / statement-only），标签随卡走，不允许事后升级。
6. 合并（integrator）。integrator 是唯一可以把通过门禁的结果合进 publication 分支的角色；组长可以提交和推送自己的分支，但从不 force-push，也从不改写他人分支。

链条之外还有两条回路和一条横切面。回路一：worker 受阻或租约过期时保留现场暂停，dispatcher 恢复后重派，禁止“硬编一个假结果”继续跑。回路二：blocker 与 direction_update 沿结果卡回流给组长和主控，触发局部 DAG 的重排。横切面是监督快照：checkpoint、语义账本、ETA 与产物在每个阶段都被汇总，组长每 30 分钟写一份 research brief——这正是 §07 那张进度 DAG 的数据来源。

宇宙监督项目复用同一条链，只是把“编译 gate”换成三道门：schema 校验（类的量化、拓扑、genericity 写全）、一手文献核对（不确定的引用一律标 unresolved）、以及数值实现门——自引力数值在 formulation 与 audit 两道门通过之前不启动。它的完成判据同样写得毫不含糊：一个节点完成 = 有产物 + 有验证证据；HTTP 成功、输出长度或 agent 共识都不算完成。

05Perelman 项目：逻辑 DAG 与前瞻式开发

Perelman 这边的分组不按文件夹名字划分，而是先把证明的逻辑依赖列成一张 canonical DAG，再在图上找可以提前推进的叶子：

左侧主链是 M0 到 M8 的顺序依赖；右侧的三条绕行边是跨层依赖（M1→M4、M2→M4、M3→M5）。颜色是当前证据状态，不是完成度百分比。

这张图表达的是数学依赖，不能直接当任务队列用——Lean 里许多依赖还没有成熟的 API，过早冻结目标只会产出一堆 statement-only 文件。真正的调度图还要回答三个问题：哪些依赖已经通过编译 gate？哪些只是条件接口？哪些可以在上游完成之前先做？于是同一张图展开成五个长期研究组：L1 Lean 基线（integrator）、L2 上游适配（scout）、L3 解析关键路径（builder）、L4 几何关键路径（builder）、L5 拓扑与审计（auditor）。

前瞻式开发：假设前面都证明好了

把逻辑上依赖的内容并行化，靠的是“前瞻式开发”：假设上游都证明好了，先推进后面的证明。关键动作不是给后续任务一个假定为真的 theorem，而是把假设写进接口，并让接口的语义等级保持可见：

一般流形热核尚未完成时，解析组仍然可以并行推进三件事：欧氏 Gaussian 可以是 kernel-checked 的模型定理；条件接口显式写出正则性、可积性、domination 等假设；下游 consumer 在接口上先行编译。等一般流形定理后来出现时，接入一个满足接口的 producer 即可。同样，几何组先完成不依赖曲率的 GHSpace 结果，拓扑组先完成识别证书和反例审计。这样做的工程价值有四条：未来任务的输入格式在上游完成之前就稳定下来；假设缺失、方向错误和 API 不匹配会被提前发现；worker 不必等待整条证明链闭合；前瞻产物不会因为“编译通过”而被误标为一般数学结果。

06宇宙监督项目：每个场论一个组

宇宙监督猜想的分组方法换了刀法：目前所有的场论设定，都各分出一个小组。仓库把猜想空间切成四个互不泄漏的类——渐近平坦弱监督的真空通用类（AF-WCC-VAC-GEN）、强监督 C2 真空类（AF-SCC-C2-VAC-GEN）、强监督 C0 真空类（AF-SCC-C0-VAC-GEN）、以及 Einstein–scalar 球对称类（AF-WCC-SCALAR-SPH）——并立为硬决策：四类永远分开，禁止跨类泄漏，也禁止把结论写成含糊的“C0 或 C2”。每个类有自己的 schema、falsifier 和产物目录；跨类只共享猜想账本和证据规则。

类之上是四个职能组长加一个 Flash 执行池，构成这个项目的 P1 与 P2；每个组和组内节点同样带 ETA 与产物标记（数据来自仓库的 research map，快照 2026-09-11）：

组内节点也按同一纪律管理：F0 分类法已交付 formulation_taxonomy.yaml；F1 真空 schema 进行中（ETA 2 d）、F2 的 C2/C0 拆分排队（4 d）；文献组的 L0 定理账本骨架依赖 F0，L1 一手核对再依赖 L0 与 F1；数值组的 N0 平空间标量波测试是所有自引力计算的前置。跨组依赖边只有五条（schema / scope / calibration / gate / class-binding），全部显式记在 map 里。当前组合计 20 个 active agent、157 / 880 agent-hours，依赖关键路径约 13–21 个日历日——这个数字随实测吞吐滚动更新，而不是拍出来的。

这个项目还多一条 Perelman 项目没有的规矩：在宣称 swarm 优势之前，先跑等预算基线。四臂等预算消融（单强模型 / 自一致性 / 独立廉价 agent / 廉价 agent + 协调者）排在 audit 组的队列里，用来回答“这套结构到底买到了什么”。

07进度 DAG：超节点、ETA 与产物

一个只画节点和箭头的 DAG 是不够的。两个项目的进度图都遵守同一条规定：以研究组为超节点；每个超节点、以及组内 DAG 里的每个具体节点，都必须带两类标记——ETA（完成所需时间的当前估计）和产物数量（已交付的可审计输出），外加状态点。读者由此可以同时回答两个问题：逻辑上，哪一项依赖阻塞了后续？工程上，哪个组正在产出可消费的产物、哪个组在等上游？

下面是 Perelman 项目的超节点进度图（宇宙监督项目的等价视图在它的 research map 仪表盘里，逐节点带同样的 ETA 与产物字段）：

实线为组间依赖，组内小箭头为任务依赖；ETA 是当前计划的估计，随 blocker 与重规划滚动更新。小屏可左右滑动查看全图。带状态筛选和证据等级的交互版本：Perelman 形式化 Swarm · 进度 DAG（交互版）。

这张图现在是手工维护的静态快照。下一步是由 queue、checkpoint、result card、compile gate 和语义账本自动生成 swarm-state.json，页面只负责渲染：一个任务只有在真实 artifact、编译记录和审计结果变化之后，才会改变节点状态。组长可以继续调整局部方向，主控可以继续重排全局优先级，而人类看到的始终是同一份可追溯的 DAG。