Poincaré 形式化 Swarm · 人类主控看板

用于主控交接、监督和 ETA 判断。所有状态都必须回到 queue、checkpoint、result card、编译门禁与独立审计证据。

快照：2026-09-11 最新可靠远端读取 · 独立 ai4math-swarm 不计入
ophis-gpu verified86compile gate 通过，不等于数学完成
运行中4task-level；不把 shell 子进程算 worker
排队38含 leader 递归导入的 child tasks
语义 blockers23精确 closure：0
admission96 / 128adaptive target / hard cap
读数规则：“verified”只表示可复现编译门禁通过；只有构造输入、下游 checked use、独立 rebuild、axiom audit 和语义审查全部齐全，才能关闭具名 blocker。当前没有无条件完整 Poincaré 证明。

M 与 L 的含义

M = Mathematical milestone：M0 到 M8 是数学主干里程碑，描述从工具链、流形几何、热核与抛物分析、DeTurck 短时流，到熵/约化体积、κ-非塌缩、canonical neighborhoods、手术灭绝和最终拓扑识别的依赖链。

L = Lifecycle / control layer：L0 到 L3 是 swarm 控制生命周期层：L0 人类 PI/主控，L1 数学组长，L2 独立 executor 进程，L3 verifier/证据层。L 编号表示控制职责，不代表数学难度。

进度条：百分比表示证据和工程闭合度估计，不是已证明定理百分比。block 只有在构造输入、编译、下游 checked use、独立 rebuild、axiom audit 和语义审查全部完成后才算关闭。

可展开数学 DAG：M0 → M8

M0 · Lean / toolchain consensus已建立固定 Lean/mathlib pin、clean build、declaration manifest、禁止公理扫描。
↓
M1 · 流形几何frontiermetric、connection、curvature、volume、IBP；U1–U5 / I1 / I3 仍需实质构造。
↓
M2 · 热核与抛物分析frontieradmissible domain、manifold heat kernel、semigroup、regularity；欧氏模型不能替代一般流形结果。
↓
M3 · DeTurck short-time flow依赖前置需要严格抛物 producer、正则性与 continuation criterion；当前主要是接口和局部模型。
↓
M4 · volume / IBP / entropy依赖前置F/W、reduced volume、时间依赖积分和全局拼接仍未完成。
↓
M5 · κ-noncollapsing / compactness依赖前置需要从已证明的分析和几何输入转移到紧性与非塌缩。
↓
M6 · κ-solutions / canonical neighborhoods未关闭不能由 conditional interface 或模型卡片替代分类定理。
↓
M7 · surgery / extinction未关闭手术控制、奇点尺度、灭绝链和拓扑消费仍缺实质证据。
↓
M8 · topology recognition / Poincaréstatement-only目标陈述存在；当前没有完整无条件 Lean 证明。

可展开工程 DAG 与验收门

控制面 → 执行面

queue schema → dependency admission → 独立 worktree → worker process group → checkpoint/heartbeat → result card。

验收：schema-valid task、依赖满足、heartbeat 新鲜、日志和 artifact 可定位。

执行面 → 证据面

result card → compile gate → axiom/declaration audit → semantic review → downstream consumer → promotion。

验收：不得用 TASK_DONE 掩盖 gate failure、模型结果或未完成审计。

恢复 DAG

SSH/relay 失败 → 保留 state/worktree → bounded retry → 从 checkpoint 恢复 → 重新验证 source hash。

验收：不删除现场，不重复计算已完成结果。

发布 DAG

worker branch → integrator batch → clean build → audit snapshot → publication branch → blog deployment。

验收：高频 push 只推送已审阅的控制面和证据，不把未跟踪实验文件混入。

ETA：按证据层级估计

时间窗合理目标不能据此声称
未来 24 小时更多真实 child admission；M0–M5 的局部编译 artifact、反例、适配和条件接口。不能声称任何完整 Perelman 层级已经关闭。
数天到一周若 leader 递归持续健康，可形成一批可复现局部 lemma、上游兼容矩阵和审计账本。不能把 queued/verified 数量线性换算成证明百分比。
数周到数月可能完成若干关键接口的真实 downstream consumer，并减少部分具名 blocker。不能跳过 M3–M7 的串行分析、几何和奇点输入。
完整主干仍按多月到多年规划，取决于非平凡数学投入和独立 kernel/axiom/semantic audit。当前数据不支持“几天完成完整 Ricci flow”。