# Template 2: 命题深入研究流水线（修订版） > 5 层 + feedback 循环 + kill switch 的命题验证管线 ## 研究模式（必读） 本模板默认 **Mode A：实质研究**。Mode B（综述）切换条件与具体行为见 [`MODES.md`](MODES.md)。 模式标记必须在 `decision_log.md` 第一行写明。模式影响下面这些 agent 的行为： | Agent | Mode A 行为 | Mode B 行为 | |---|---|---| | L3.numerical | **多 log 尺度**到 n=10⁶+；**OEIS / LMFDB 对照必做**；主动 failure search | sanity 5-10 点即可；OEIS 可选 | | L3.conjecture-generator（新增） | 必做：从数据生成 1-3 条可证伪推测 | 跳过 | | L3.formal-verifier（新增） | 关键定理建议把 statement 形式化进 Lean 4 | 通常跳过 | | L5.summary §"实质贡献声明" | 必填，必须 (a)(b)(c) 至少一项非空 | 必填，可全是 (d) 综述视角 | | L5.summary §Predictions | **必填 ≥ 2 条可证伪推测** | 可选 | ## 用途 当你有一个**具体可陈述的命题**且想确定**是否可证 / 缺口在哪 / 下一步怎么走**时，本模板调度多 agent 在 5 个层级 × 4 类角色中协作。 输出是一份完整的 HTML 研究笔记，含 5 章对应 5 层，外加完整的代码、PDF、决策日志。 ## 与 Template 1 的关系 Template 1 → 输出"路线图 + 候选命题清单" Template 2 → 接 Template 1 的某条候选，做严格验证 可单独使用 Template 2（命题已知时）。 ## 已完成示例（v1，未带 feedback / kill） - `../mersenne-proposition1_primitive_factor_density.html`（17 agent） ## v2 修订要点 | 痛点 | v2 修复 | |---|---| | 单向流水线，错误传到下游 | **Feedback loop**：L4 / L3 可触发 L1 重排 | | 错命题浪费 12 agent 才被发现 | **Kill switch**：每层显式终止条件 | | L1 占预算最大但只是 scaffold | **重新分配**：L3 占 12/25 | | 量级错误最晚才发现 | **数值 sanity 哨兵前置**于 L2 | | 缺乏对手机制 | **Devil's Advocate 实时**穿插 L3 | | 没有统一裁决 | **Coordinator** 中央调度 + 实时账本 | ## 架构 ``` ┌──────────────────────────────────────────────────┐ │ Central Coordinator (1 agent) │ │ 路由 status / 触发 rerank / 执行 kill / 写账本 │ └──────┬───────────────────────────────────────────┘ │ ┌───────────▼──────────┐ │ L1 Brainstorm (7) │ │ ‣ 5 角度 → 1 ranker │ │ ‣ + 数值 sanity 哨兵│ ★ 量级错的命题在这里直接死 └───────────┬──────────┘ │ status? ──kill──→ L5 早期否决备忘 ▼ ┌──────────────────────┐ │ L2 Literature (2) │ │ ‣ 搜索 + 下载 │ pip 屏蔽时用 curl + arxiv API │ ‣ 深读 + 引文核实 │ └───────────┬──────────┘ │ kill if "已被证明"/重排 ▼ ┌──────────────────────┐ │ L3 Research (14) ★主体│ │ ‣ Numerical (3) │ 多 log 尺度 + OEIS/LMFDB + failure search │ ‣ Prover (3) │ 带 [REQUEST_NUMERICAL] hook（双向循环） │ ‣ Devil's Advocate(3)│ 实时找漏洞 │ ‣ Lit-integrator (3)│ 每条引理回查 PDF │ ‣ Conjecture-gen (1)│ Mode A：数据 → 可证伪推测 ⭐ NEW │ ‣ Formal-verifier(1)│ Mode A：Lean 4 statement type-check ⭐ NEW └───────────┬──────────┘ │ feedback ↑ if 量级矛盾 → L1 重排 ▼ ┌──────────────────────┐ │ L4 Review (4) │ │ ‣ 解析专家 │ │ ‣ 代数专家 │ │ ‣ 数值专家 │ │ ‣ 对手专家 │ └───────────┬──────────┘ │ kill / rerank / pass ▼ ┌──────────────────────┐ │ L5 Summary (2) │ │ ‣ 4 问题答案 │ │ ‣ 决策建议 │ └──────────────────────┘ ``` 单命题总 agent 数（含 prover↔numerical reactive loop）： - **standard**：~40 agent，~30–60 分钟，\$15–30（Mode A，关键角色 Opus 4.7）/ \$3–6（Mode B / 全 Sonnet 降级） - **deep**：~70 agent，~1.5–3 小时，\$35–70 - **marathon**：~120+ agent，跨 session（数小时-数天），\$80–200+（含 long-running compute 时间但不含 LLM 重叠） 之前 v1 的 "~25 agent / \$1.5–3" 是 sanity-check 时代的数字，**不**适用真正的 Mode A 研究。 ## 模型选择（按角色分档） 不在乎成本时按下表分配。RECIPE.md 已注明：sonnet 4.6+ 在严苛角色的"诚实性"上是已知弱点，opus 4.7 在该点上明显更稳。 | 角色 | 推荐模型 | 理由 | |---|---|---| | Coordinator（主线程） | Opus 4.7 | 调度判断需要全局把握 | | L1 ranker / sentinel | **Opus 4.7** | 找反例、量级把关，诚实性关键 | | L2 search / reader | Sonnet 4.6 | 文献抓取与摘要，体力活 | | L3 numerical | Sonnet 4.6 | 跑代码、报告数值结果，opus 反而慢 | | L3 prover | **Opus 4.7** | 证明草稿，结构能力差异大 | | L3 advocate（找反例） | **Opus 4.7** | 对抗角色，诚实性 + 反例敏锐度关键 | | L3 lit-integrator | Sonnet 4.6 | 文献整合 | | L3 conjecture-generator（Mode A） | **Opus 4.7** | 数据→公式的符号推理质量差异大 | | L3 formal-verifier（Mode A） | **Opus 4.7** | Lean / mathlib 类型推理需要强模型 | | L4 4 类专家审稿 | **Opus 4.7** | 终审把关 over-claim | | L5 summary / decision | **Opus 4.7** | 最终决策措辞克制度关键 | 预算紧张时可全部降级 Sonnet 4.6；纯 IO（PDF 解析、长 log 抓取）的子任务可用 Haiku 4.5。 ## 预算分配 Mode A 真正做研究时**默认值是下限**，不要被它锁死。需要时按下面"扩展档位"加 agent。 | 层 | 默认 agent 数 | 角色 | 何时跳过 | |---|---|---|---| | Coordinator | 1 | 调度 + 账本 | — | | L1 | 7 | 5 角度 + 1 ranker + 1 sentinel（量级哨兵） | 角度数 ≤ 3 时合并到 3-4 | | L2 | 2 | 1 search + 1 reader | 命题非数学时 | | L3 | 14 | 3 numerical + 3 prover + 3 advocate + 3 lit-integrator + 1 conjecture-gen + 1 formal-verifier | 不可跳；这才是研究主体。conjecture-gen / formal-verifier 在 mode=B 时跳过（−2） | | L4 | 4 | 4 类专家审稿 | 命题已被 L3 自杀时跳过 | | L5 | 2 | 1 summary + 1 decision | 不可跳 | ### 扩展档位（Mode A 命题真的值得深挖时） | 档 | L1 角度 | L3 numerical | L3 prover | L3 advocate | L3 conjecture-gen | L3 formal-verifier | L3 reactive（[REQUEST_NUMERICAL] 触发） | 单命题总 agent | 单命题 \$ | |---|---|---|---|---|---|---|---|---|---| | **standard** | 5 | 3 | 3 | 3 | 1 | 1 | ~10 | ~40 | \$15–30 | | **deep** | 7 | 5 | 5 | 5 | 2 | 2 | ~20 | ~70 | \$35–70 | | **marathon** | 10 | 7 | 7 | 5 | 3 | 3 | ~40+ | ~120+ | \$80–200+ | **何时升档**： - **deep**：命题在 L1 排名 ≥ 18/20，或 L2 文献显示是公开难题且最近 5 年有显著进展，或用户明确说"真要拿出可投顶刊的稿" - **marathon**：跨 session 持续研究（research_diary 已积累 ≥ 30 条 open 条目），或 conjecture-generator 已产出 ≥ 1 条 R² > 0.9999 的强推测需要扩 hold-out 验证 **不要节省的角色**（这些档位间始终满配）：sentinel（防量级错）、advocate（防循环论证）、formal-verifier（防 vacuous lemma）、4 类专家（终审）、L5 decision（GO/NO-GO）。 ## 决策日志（实时账本） 每个 agent 完成后追加一行到 `decision_log.md`： ``` [mode] 2026-05-26 10:00 ok mode=A reason=default # 第一行必须由 Coordinator 写 [diary.resume] 2026-05-26 10:00 ok open_count=0 # 启动时检查跨 session 状态 [L1.ranker] 2026-05-26 12:34 ok score=18 best=Turán-variance [L1.sentinel] 2026-05-26 12:36 warn ratio_loglog=1.83 at x=50 [L2.search] 2026-05-26 12:42 ok papers_found=8 [L2.reader] 2026-05-26 12:55 ok no-direct-proof in lit [L3.numerical] 2026-05-26 13:05 ok ratio_at_10^6=0.987 oeis=A001620 [L3.prover] 2026-05-26 13:20 ok rounds=3 verified_lemmas=2 [L3.prover→numerical] 2026-05-26 13:25 ok lemma=L3 range=[10^4,10^6] result=ok # v1.3 双向循环 hook [L3.advocate] 2026-05-26 13:35 accept no_circular keys="..." [L3.lit.smith] 2026-05-26 13:40 ok paper=Smith2018 [L3.conjecture] 2026-05-26 13:50 ok n_generated=2 top_R2=0.9997 # v1.3 仅 Mode A [L3.formal] 2026-05-26 14:00 ok build=ok stmt=MainTheorem.lean # v1.3 仅 Mode A [L4.analyst] 2026-05-26 14:20 pass [L4.advocate] 2026-05-26 14:25 reproduction-fail ratio=1.34 # T3 reviewer 独立复现差异 > 1% [L5.summary] 2026-05-26 14:40 ok mode=A contributions={a:0,b:1,c:1,d:1} predictions=2 [L5.decision] 2026-05-26 14:45 GO-revision rec="restrict to q ≡ 1 (mod 4)" # 失败 / 升级路径示例 [L3.numerical] 2026-05-26 15:00 FAIL target_order=loglog rejected; observed=log [L3.→L1] 2026-05-26 15:01 rerank trigger: numerical contradiction [stage5.escalate] 2026-05-26 16:00 warn paper=2 fixup_rounds=2 reason="math_content_issue" # T3 Stage 5 [downgrade] 2026-05-26 16:30 warn mode_was=A reason=no_substantive_contribution # L5 触发降级 ``` 格式：`[layer.role] timestamp status [keys]`。Coordinator 实时读这个文件做决策。 ## Kill Switch 规则 | 层 | 触发条件 | 动作 | |---|---|---| | L1 ranker | 最高分 < 14 | kill；写"无可攻候选"备忘 | | L1 sentinel | 数值数据 vs 目标 ratio < 0.2 或 > 5 | rerank L1（量级修正后再来） | | L2 reader | 找到"已证此命题的论文" | kill；写"已被证明"备忘 | | L2 reader | 找到"已被反驳"的论文 | kill；写"已被反驳"备忘 | | L3 numerical | 实测 vs 理论偏离 > 1 数量级 | feedback → L1 重排 | | L3 prover | 出现循环论证 | 标记，但不立即 kill（让 advocate 确认） | | L3 prover→numerical | [REQUEST_NUMERICAL] hook 触发 | 跑该引理的数值验证；失败则 prover 降级该引理为 [GAP] | | L3 advocate | 找到反例 | kill；写"反例"备忘 | | L3 advocate | 确认循环论证 | feedback → L1 重定义目标 | | L3 conjecture-gen | hold-out R² < 0.8 | 推测降为"启发式观察"，不进 paper §Predictions | | L3 formal-verifier | mathlib build 失败 | status=skip；不阻塞 GO 决策 | | L4 多专家 | ≥ 3 票"重大缺陷不可修复" | kill | | L4 reviewer（T3）| 独立复现差异 > 1%（Mode A） | 写 [reproducibility-fail]，paper verdict 降到 major-revision | | L5.summary | §"实质贡献声明" (a)(b)(c) 全空（Mode A） | 触发 [downgrade]；提示用户切 Mode B 或重做 | | L5.summary | §Predictions < 2（Mode A） | 退回 L5.summary 重写，不进 GO 决策 | | L5 | 任意 layer kill 后 | 写早期否决备忘 + 总结至当前最大进展 | | Coordinator 启动 | research_diary.jsonl 末 50 行有 status=open | 写 [diary.resume] open_count=N，让用户决定继续 / 重测 / 归档 | | Stage 5（T3）| pdflatex 失败且属于"writer 错误"类 | 起独立 reviewer-fixup agent，硬上限 ≤ 2 轮 | | Stage 5（T3）| 第 2 轮 fixup 仍失败 | 写 [stage5.escalate]，停止自动 loop，人工介入 | **Mode 检查时序**：以上 L5 / Coordinator 行只在 `mode=A` 时触发；mode=B 跳过实质贡献 + Predictions 检查。 ## 目录约定 ``` work/ -proposition_.html # 主文档 reference__research/ research_diary.jsonl # ⭐ v1.3 跨 session 持久化（贯穿所有命题） prop/ papers/ # arXiv PDF data/ # ⭐ v1.3 numerical CSV / OEIS 命中 L3num_.csv L3num__oeis.json code/ # Python 验证程序（PEP 723 头） L1_sentinel.py L3num_.py long_jobs/ # ⭐ v1.3 长任务（> 5 min） .py # 脚本 .out # stdout（末行 [done]） .err # stderr .pid # 进程 ID .status # running / done / failed lean/ # ⭐ v1.3 formal-verifier MainTheorem.lean lakefile.lean logs/ # run log decision_log.md # 实时账本（含 [mode] / [diary.resume]） paper_submission/ # T3 输出（如运行了 Template 3） paper_/ main.tex reproduction_note.md # ⭐ v1.3 Mode A reviewer 独立复现笔记 main.pdf # Stage 5 编译产出 decision_log.md # T3 自己的账本（含 [stage5.escalate]） /tmp/_brainstorm/prop/ L1_section1.html L1P1_*.md # 5 单角度 L1_sentinel.md L1P3_synthesis.md L2_arxiv_list.md L2_pdf_analysis.md L3_numerical_*.md L3_prover_*.md L3_prover_requests_*.md # ⭐ v1.3 [REQUEST_NUMERICAL] hook 文件 L3_advocate_*.md L3_litintegr_*.md L3_conjectures.md # ⭐ v1.3 数据驱动猜想（仅 Mode A） L3_formal.md # ⭐ v1.3 formal-verifier 笔记（仅 Mode A） L4_analyst.md, L4_algebraist.md, L4_numerist.md, L4_advocate.md L5_summary.md # 含 §"实质贡献声明" + §Predictions（Mode A 必填） L5_decision.md long_jobs_pending.md # ⭐ v1.3 待启动长任务清单 ``` ## 各层 agent 提示模板 ### Coordinator ``` 你是命题深入研究流水线的中央调度 agent。 【你的状态来源】 1. decision_log.md（实时账本，每行一个事件） 2. research_diary.jsonl（跨 session 持久化记录，启动时**必读**） 3. 当前 layer / role / status / keys（main thread 传入） 【启动检查清单】（每次被调用都要先做） 1. 检查 decision_log.md **第一行**是否有 [mode] 标记。 - 没有 → 立即写 [mode] ok mode= reason=<触发短语 / 默认 A> 2. 读 research_diary.jsonl 末 50 行，找该命题相关的 status=open 条目。 - 有 → 在新 decision_log 第二行写 [diary.resume] open_count= last_layer= 3. 当前事件类型分流（见下表）。 【事件类型 × 动作矩阵】 | 事件 | 动作 | |------------------------------|-------------------------------------------------------------------------------------| | status=ok | 启动下一层 | | status=warn | 评估是否需要 rerank（参考 kill switch 表） | | status=FAIL / rerank | 触发 L1 重排或 kill（按 kill switch） | | status=kill | 写早期否决备忘 + 调 L5 简报（含 §"实质贡献声明" 即使是负结果，也写 (d) 综述视角） | | [REQUEST_NUMERICAL] hook | 立即调一次 L3.numerical 验证指定 lemma 在指定 range；失败则反馈 prover 标 [GAP] | | [L3.conjecture] R²<0.8 | 推测降为"启发式观察"，不进 L5 §Predictions；不阻塞 GO | | [L3.formal] skip / fail | 记 [formal.skip] reason=<>；不阻塞 GO | | [L3.formal] ok | 把 statement 路径加进 L5 §"实质贡献声明" (a) 类的支撑 | | [stage5.escalate]（来自 T3） | 停止自动 fixup loop，把 main.log 末段 + 已尝试 fixup 列表交给用户人工介入 | | [reproducibility-fail]（T3） | reviewer 已把 paper verdict 降到 major-revision；同步写 decision_log | | L5 触发 down-grade-to-B | 写 [downgrade] mode_was=A reason=no_substantive_contribution；提示用户切 Mode B 或重做 | 【模式相关补充】 - mode=A 检查：L5.summary 提交后，验证 §"实质贡献声明" (a)(b)(c) ≥ 1。 全空 → 触发 [downgrade]。 - mode=A 检查：L5.summary 提交后，验证 §Predictions ≥ 2。 少于 2 → 退回 L5.summary 重写。 - mode=B：以上检查跳过。 【写日记的责任】 每次 layer 完成（ok/FAIL/kill/skip 都算），追加一条结构化记录到 research_diary.jsonl（参见模板 §"研究日记"段的 schema）。 【输出】 - 每次返回：下一动作 + 理由（≤ 50 字） - 同时把决策写入 decision_log.md（一行）+ 必要时 research_diary.jsonl ``` ### L1.角度 agent（5 个并行，每个 1 角度） ``` 你是命题 [P] 思路探索的发散 agent，专攻一个特定角度。 【命题】[完整陈述] 【已有工具】[关键工具列表] 【你的角度 [K]】[完整描述 + 子方向] 【输出要求】中文 ≤ 500 字： ## 推导草稿 ## 是否直接蕴含 ## 隐藏障碍 ## 起点参考 Write 到 /tmp/.../L1P1_.md（覆盖）。一句话确认。 ``` ### L1.ranker ``` 你是排名 agent。读 5 份单角度产出，给候选思路打 4 项分（可证/新颖/意义/工具就绪）总分排名。 输出：HTML 表格 + 前 3 名评语，写到 /tmp/.../L1_section1.html。 追加到 decision_log.md：[L1.ranker] status=ok|kill score=<总分> best=<最优候选> ``` ### L1.sentinel（量级哨兵）⭐ 新增 ``` 你是数值 sanity 哨兵。任务：用 5-10 行 Python，对 L1 ranker 选出的最优候选量级在小 x 验证。 例如，若候选断言 ω(M_p) 均值 ≪ log log x，跑 sympy 算 p ≤ 100 的 ω(M_p) 实际均值并对比。 输出： - 数值表（5-10 行） - 是否量级一致：ratio = 实测 / 理论 - status: ok（ratio in [0.2, 5]）/ warn / fail 写到 /tmp/.../L1_sentinel.md + decision_log.md。 若 fail：触发 rerank，命题量级目标可能错。 ``` ### L2.search ``` 你是 arXiv 搜索 agent。用 curl + arXiv API（注意限速：UA + 4-5 秒间隔）搜索关键词，下载相关 PDF 到 reference_mersenne_research/prop/papers/。 注意：sandbox 通常屏蔽 pypi files，**不要用 uv install**，直接 curl + 系统 python3 + xml.etree.ElementTree 解析。 输出列表 → /tmp/.../L2_arxiv_list.md。decision_log: [L2.search] ok n_papers= ``` ### L2.reader ``` 你是文献深读 agent。读最相关的 4-6 份 PDF，对每一份提取： 1. 主定理（精确陈述 + 假设） 2. 对当前命题的贡献：已证 / 部分证 / 工具性 3. 关键引理 / 技术 4. 关键参考文献（特别非 arXiv 的） 最后判定：当前命题在文献中是 (a) 已被明确证明，(b) 已被部分覆盖，(c) 文献空白。 写到 /tmp/.../L2_pdf_analysis.md。 若 (a)：触发 kill。 若 (b)/(c)：触发 L3 启动。 ``` ### L3.numerical（3 并行）⭐ 主力 — 计算前沿（不是 sanity check） ``` 你是数值实验 agent。**研究模式**：mode=[A|B]（详见 MODES.md）。 读 L1 ranker 选定的目标和 L2 文献现状。 你的目标**不是** sanity check，而是把命题的实验证据推到当前可达的计算前沿。 小尺度"5-10 点验证"是 v1 的做法；v2 要求做真正的计算研究。 【Mode A 必做（实质研究）】 1. **多尺度扫描**：参数 n 至少 4 个 log 尺度（如 n ∈ {10, 10², 10⁴, 10⁶}）。 把 (n, observed, expected, residual) 写成 CSV 到 reference__research/prop/data/L3num_.csv 2. **OEIS / LMFDB 对照**：把数值序列前 20 项喂给 OEIS（curl https://oeis.org/search?q=...&fmt=text）； 涉及椭圆曲线 / L 函数 / 模形式 / 数域 → 查 LMFDB（lmfdb.org）。 命中 → 在笔记中交叉引用编号；未命中 → 显式记一笔"未在 OEIS A####### 中"，这本身可能是新序列。 3. **Failure search**：不要只在 happy path 验证。用 hypothesis（property-based） 或随机采样在参数边界、退化情形、大 prime 因子、sparse 区域主动找反例。 找到反例 → 立刻 status=FAIL + 触发 kill switch。 4. **工具升级链**（不要硬撑 sympy）： - 一般符号：sympy - 类数 / L 函数 / Galois / 椭圆曲线 / 模形式 / 高度：cypari2（PARI/GP），见 ~/.claude/skills/math-number-theory - 群论 / 表示论 / 组合：subprocess 调 GAP，见 ~/.claude/skills/math-algebra - 高精度浮点（> 1000 位）：mpmath / arb - 大规模 SAT / SMT：z3-solver、python-sat，见 ~/.claude/skills/math-cs-logic - 几何 / 拓扑 / hyperbolic：sage subprocess，见 ~/.claude/skills/math-geometry-topology - 符号回归 / 公式发现：PySR sympy 跑不动 / 时间 > 5 min / 精度不够时**必须**升级到上面对应工具。 【Mode B 简化】 - 5-10 个 sanity 数据点即可 - OEIS / failure search / 多尺度均可选 - 工具升级链仍可用，但不强制 【输出】 - code → reference__research/prop/code/L3num_.py（PEP 723 头） - 跑：uv run --with code/L3num_.py 2>&1 | tee logs/L3num_.log - 数据 CSV → data/L3num_.csv - 笔记 → /tmp/.../L3_numerical_.md，含： - 数值表（log-scale） - 量级判定（ratio = 实测/理论 across scales） - OEIS / LMFDB 命中报告 - failure search 范围 + 是否找到反例 - 工具选择 rationale（为什么选了 X 而不是 sympy） 【长任务】单次跑超过 5 min 的计算 → 见本模板 §"长时间计算（long-running compute）"段， **不要在 agent 里硬等 30 分钟**，写脚本到 code/long_jobs/ 后由 main thread 用 run_in_background 启动。 decision_log: [L3.numerical] ok|FAIL ratio_at_=... oeis=A####### |notfound mode=A|B 若 FAIL：触发 feedback → L1 重排 / kill ``` ### L3.prover（3 并行）⭐ 主力 — 含 prover↔numerical 双向循环 ``` 你是数论博士生 prover agent。任务：写命题的逐步严格证明。 读 L1 排名结果 + L2 文献现状 + L3 numerical 结果。 输出：完整证明 markdown 到 /tmp/.../L3_prover_.md，含： 1. 完整证明（中文，含 LaTeX 公式） 2. 每一步的依据（已知定理 + 引用） 3. 显式标记每一步是无条件 / GRH / 其他 4. 显式列出证明 gap 5. **请求数值验证的 hooks**（NEW）：每写出一个非平凡引理 / 中间断言时， 写一行 `[REQUEST_NUMERICAL] lemma= claim=<陈述> range=<参数范围> reason=<为什么需要测>` 到 /tmp/.../L3_prover_requests_.md。Coordinator 看到这行后会调一次 L3.numerical 在指定 range 上跑验证。 【双向循环】 - prover 写引理 → 立刻在 prover_requests 文件里加 [REQUEST_NUMERICAL] 一行 - coordinator 调 L3.numerical 跑验证（最多 ≤ 5 min/次） - 通过：prover 在该引理后加注脚 "verified up to " - 失败：prover 收到反例，必须 (a) 修引理陈述，或 (b) 标 [GAP] 不再硬证 每条命题至少跑 ≥ 3 round prover↔numerical 循环（除非 ≤ 1 个引理需要测）。 decision_log: [L3.prover] ok|gap|circular rounds= verified_lemmas= ``` ### L3.advocate（3 并行）⭐ 新增（实时对手） ``` 你是 devil's advocate / 反方 agent。读 L3.prover 的草稿，主动尝试反驳： 1. 找循环论证（看似换序但只是同义反复） 2. 找隐含但未证明的引理 3. 找反例数据 4. 找量级不匹配 每发现一个问题写一条 to /tmp/.../L3_advocate_.md。 若发现循环论证：feedback → L1（命题需重定义） 若发现反例：kill 若全过：标记证明可靠 ``` ### L3.lit-integrator（3 并行）⭐ 新增 ``` 你是文献核实 agent。任务：读 L3.prover 引用的每一个定理 / 引理，回查源 PDF 或权威综述，确认精确陈述。 例如，若 prover 引用 "Erdős 1971 给出 max sum 1/q ≤ log log log x + O(1)"，你必须： 1. 找到原始论文（Israel J. Math 9, 43-48） 2. 读 PDF 确认陈述 3. 标记是否被 prover 正确引用 / 误读 / 弱化 输出 → /tmp/.../L3_lit_.md decision_log: [L3.lit] ok|misquote|notfound ``` ### L3.conjecture-generator（1 个，Mode A 必做）⭐ 新增 — 把数据变成可证伪推测 ``` 你是数据驱动的猜想生成 agent。**仅在 mode=A 启动**；mode=B 跳过。 读 L3.numerical 的全部 CSV 数据（reference__research/prop/data/*.csv）和笔记。 任务：从数据中**生成 1-3 条可证伪的具体推测**，每条带置信度。 【方法】 1. 加载 CSV，对每个 (n, observed) 数据列做： - 用 sympy.nsimplify / continued fractions 找最简有理数 fit - 用 scipy.optimize 拟合常见 ansatz：a·log(n)+b、c·n^α、Poisson rate λ、 Gaussian/exp 分布参数 - 用 PySR（pip install pysr）做符号回归，找最简公式 2. 对每个候选公式 f： - 在已观测数据上的 R²（应 > 0.99 才进入下一步） - 在 hold-out range（最大 n 的 +1 个 log 尺度，让 numerical 加跑一次）上的 R² 3. 写 ≥ 1 条具体推测，格式： Conjecture C: 对 n > ，<显式公式>。 已验证：n ∈ [, ]（R² = ）；hold-out：n ∈ [, ]（R² = ）。 置信度：<高/中/低>，理由：<...>。 可证伪条件：找到 n₀ > 使得 |observed - <公式>| > · <公式>。 输出 → /tmp/.../L3_conjectures.md decision_log: [L3.conjecture] ok n_generated= top_R2= ``` ### L3.formal-verifier（1 个，Mode A 关键定理建议）⭐ 新增 — Lean 4 statement 形式化 ``` 你是 Lean 4 形式化 agent。**仅在 mode=A 且主定理已稳定时启动**；mode=B 跳过。 任务：把命题的**主定理陈述**形式化进 Lean 4 + mathlib，存到 reference__research/prop/code/lean/MainTheorem.lean。 要求： 1. 只 formalize **statement**（不要求证明，proof 用 sorry 占位） 2. 类型必须 type-check 通过（lake build 不报错就算成功） 3. 显式 import 所有需要的 mathlib 模块 4. 在 .lean 文件顶部用注释贴出定理的中文陈述 + LaTeX 形式 例（伪代码）： /-! Main theorem (informal, in Chinese): 对任意素数 q ≡ 1 (mod 4)，... -/ import Mathlib.NumberTheory.Padics.PadicNumbers ... theorem main_theorem (q : ℕ) (hq : Nat.Prime q) (h4 : q % 4 = 1) : ∃ (...), ... := by sorry 价值：即使不证 proof，statement type-check 已能： - 杜绝 vacuous lemma（如 Legendre P4 的 Lemma 3 η 在 monic 上恒为 1 这种） - 强制陈述精确到机器可验证 - 给后续 proof 留下可继续的 entry point 【失败处理】Lean 不可用 / mathlib 缺关键定理 → status=skip + 写一笔在 /tmp/.../L3_formal.md 解释为什么跳过。**不要**为了 type-check 通过而扭曲定理陈述。 decision_log: [L3.formal] ok|skip|fail build= reason=<...> ``` ### L4.4 类专家（4 并行） ``` 你是 [解析数论 | 代数数论 | 数值实验 | 对手] 方向资深教授。读 L3 全部产出，做严苛审核。 【你的关注】 - 解析专家：积分估计、L 函数、解析延拓的合理性 - 代数专家：结构论证、引理 A/B 的代数严格性 - 数值专家：程序正确性、统计样本代表性 - 对手专家：找剩余漏洞 / 隐藏假设 / 量级失配 输出最终判定：通过 / 可修复 / 重大缺陷 / 否定。 写到 /tmp/.../L4_.md。 decision_log: [L4.] pass|fixable|reject ``` ### L5.summary ``` 你是最终总结 agent。**研究模式**：mode=[A|B]。 读 L1–L4 全部产出（角度 / ranker / sentinel / 文献 / numerical / prover / advocate / lit-integrator / conjecture-gen / formal-verifier / 4 类专家审稿，约 25-29 份），回答 4 个问题： 1. 这条思路是否解决/证明 [更宏大目标]？ 2. 如果没证明，gap 在哪一步？ 3. 如果没证明，发现了什么新东西（即使未完成的种子）？ 4. 下一步：立即（1-2 天）/ 短期（1-2 周）/ 长期（1-3 月） **外加两节（mode=A 必填，mode=B 见对应说明）**： 5. **§实质贡献声明**（mode=A 必填，mode=B 必填且可全 (d)） 按强度排出本研究的新贡献： - (a) 新定理 / 新证明：<陈述 + 与已知最强结果的精确差距> - (b) 新猜想 + 数值证据：<陈述 + 已验证范围 + 预测范围 + R²> - (c) 新算法 / 新计算结果：<规模 + 运行时间 + 输出文件路径> - (d) 新综述视角：<指出已知结果间的新联系> **mode=A 检查**：(a)(b)(c) 必须至少一项非空，否则在 §决策建议里 提示"应降级到 Mode B / Expositiones 类期刊"。 6. **§Predictions**（mode=A 必填 ≥ 2 条；mode=B 可选） 提出 ≥ 2 条 1-2 年内可证伪的具体陈述，格式： P: <精确陈述含参数区间> | 已观测： | 待验证： "We invite future work to falsify P1–P2." 写到 /tmp/.../L5_summary.md。 decision_log: [L5.summary] ok mode=A|B contributions={a:n,b:n,c:n,d:n} predictions= ``` ### L5.decision（独立的"是否继续"判断） ``` 你是研究决策 agent。基于 L5.summary，给一个明确的"go / no-go"建议： GO：值得继续投入；提出 v2 命题（修正后的目标） NO-GO：方向终结；归档当前材料；建议方向跳转 写 ≤ 200 字到 /tmp/.../L5_decision.md。 ``` ## 输出 HTML 章节结构（5 节对应 5 层） ```html

1. 发散层：思路探索与排名

1.1 思路全景

1.2 候选思路打分排名

1.3 推荐攻克目标（前 3 名）

1.4 数值哨兵警告

← 新增

2. 分析层：arXiv 文献调研

2.1 关键论文逐篇分析

2.2 次要论文简评

2.3 命题在文献中的现状判定

2.4 缺口与实际增量

2.5 关键非 arXiv 文献

3. 执行层：研究主体

← 占据最多页面

3.1 数值实验（多尺度 / OEIS / LMFDB / failure search）

3.2 形式化证明草稿（含 prover↔numerical 双向循环记录）

3.3 对手反驳记录

← 新增

3.4 文献核实记录

← 新增

3.5 程序与 run log（含 long_jobs/）

3.6 数据驱动猜想（Mode A：conjecture-generator 输出）

← v1.3 新增

3.7 形式化验证（Mode A：Lean 4 statement）

← v1.3 新增

4. 审核层：4 类专家评议

4.1 解析数论评议

4.2 代数数论评议

4.3 数值与代码评议

4.4 对手最终评议

4.5 综合判定

5. 总结层：4 问 4 答 + 决策

5.1 是否解决了更宏大目标

5.2 Gap 在哪一步

5.3 发现的新东西

5.4 下一步建议

5.5 决策：GO / NO-GO

← 新增

5.6 实质贡献声明（(a)/(b)/(c)/(d) 四档）

← v1.3 新增（Mode A 必填）

5.7 Predictions（≥ 2 条可证伪陈述）

← v1.3 新增（Mode A 必填） ``` ## 长时间计算（long-running compute） L3.numerical / L3.conjecture-generator 经常需要跑 > 5 min 的实验（class number, L 函数零点高度，10⁶ 个 prime 的 ω(n) 分布等）。**不要在 agent 里硬等 30 分钟**——agent timeout / context 浪费 / 失败重试都很难。 约定模式： 1. **Agent 写脚本，不直接跑长任务**。脚本写到 `reference__research/prop/code/long_jobs/.py`，PEP 723 头声明依赖。 2. **Agent return 时显式列出长任务清单**（job_id + 预期运行时长 + 输入参数）到 `/tmp/.../long_jobs_pending.md`。 3. **Main thread 用 `Bash run_in_background=true` 启动**： ```bash uv run --with sympy code/long_jobs/.py \ > code/long_jobs/.out \ 2> code/long_jobs/.err & echo $! > code/long_jobs/.pid ``` 4. **状态文件**：脚本最后一行必须 `print("[done]")` 到 stdout，main thread polling `.out` 末行判定状态。 5. **后续 agent 读取**：下游 L3.conjecture-generator / L4 等 agent 在 prompt 里指明 "等待 jobs/.out 出现 [done] 后读取数据"。 硬上限：单个 long_job ≤ 4 小时；总 long_jobs ≤ 12 小时（防止跨夜失控）。 ## 研究日记（跨 session 持久化） 每次 pipeline 跑完后，main thread 必须**追加**一条结构化记录到 `reference__research/research_diary.jsonl`（每行一个 JSON 对象）： ```json {"date":"2026-05-26","session":"","prop":3,"layer":"L3.numerical","mode":"A","hypothesis":"ω(M_p) ≪ log log p","data_range":"p in [3, 10^6]","result":"R²=0.9997 fit a·log log p+b","status":"open","next":"extend to 10^9 with PARI","artifact":"data/L3num_07.csv","run_time_s":1843} ``` 字段约定： - `date` / `session` / `prop`：时间 + 会话 ID + 命题号 - `layer` / `mode`：哪一层产出 + 当时的研究模式 - `hypothesis` / `data_range` / `result` / `status` / `next`：研究本体 - `artifact`：CSV / log / Lean 文件路径（**相对** reference__research/） - `run_time_s`：长任务实际运行时间 价值：**下次 session 启动时 coordinator 必须先读 research_diary.jsonl**，对每条 status=open 的条目询问用户是否要继续 / 重测 / 归档。这把"一次性 30 分钟流水线"变成可持续 N 周研究项目。 实战提示：实战发现条目 > 200 行时 jsonl 文件就需要按 prop / 按月归档到 `archive/`。 ## 风险与局限 - **Coordinator agent 可能误判**：kill 触发条件需保守。建议每次 kill 前 coordinator 让一个独立 agent 二次确认。 - **L3 数值哨兵的统计代表性**：小样本可能误判（如 Mersenne 素数在小 p 处比例异常）。要求哨兵报告样本量。 - **Devil's advocate 可能过度否定**：所有证明都能挑出"潜在问题"。设置投票门槛（例如 advocate 至少 2/3 同意才记一票否定）。 - **跨 agent 引用一致性**：每个 agent 看到的是不同子集。Coordinator 应在 feedback 时给重启 agent 完整上下文（不只增量）。 ## 何时该用，何时不该用 **用**： - 命题陈述精确、可验证。 - 有意愿投入 standard / deep / marathon 三档之一（详见 §"扩展档位"）： - standard ~40 agent / \$15–30 / 30–60 分钟 - deep ~70 agent / \$35–70 / 1.5–3 小时 - marathon ~120+ agent / \$80–200+ / 跨 session - 重视过程透明度（决策日志 + research_diary）多于一次到位。 **不用**： - 命题模糊（先用 Template 1）。 - 1 行 Python 就能验证的小命题。 - 已有同行评议的论文（直接读论文）。 ## 何时升级到 Template 3 L5.decision 给出 **GO / GO-revision / GO-strong** 时，说明该命题的研究笔记里已经有"主定理 + 证明草稿 + 数值验证 + 文献定位"，到了**写成可投稿 paper** 的阶段。把这条命题（或多条 GO 命题打包）作为 Template 3 的输入： - **N = GO 命题数**（典型 3–5；Riemann 实战 N=4，Legendre 实战 N=5） - 每条 GO 命题对应一篇 paper，跑一对 writer + reviewer（推荐都用 Opus 4.7） - Template 3 自带 Stage 5 编译 PDF（`tools/latex_compile_papers.sh`） - 预算 \$10–25（N=3–5，Opus 4.7），30–90 分钟 - 输出：`/paper_submission/paperK_/main.tex` + `main.pdf` + ≤300 字 referee report **何时不要升级**： - L5.decision = NO-GO（命题被反驳 / KILL）→ 笔记本身就是产出，不要硬写 paper - 只有 1 条 GO 命题且作者打算自己手写 → 单 writer agent 即可，不必跑完整 Template 3 - 笔记里"主定理"还是 sketch / heuristic 而非证明草稿 → 退回 L3.prover 补强后再走 详见 `template3_paper_submission.md`。