一套可直接运行的「多角色自治数学证明」研究框架。方法层复刻自两个已验证的真实开源项目（2026-08-15 逐一核验过 GitHub API / arXiv 摘要）：
| 来源 | 状态 | 贡献 |
|---|---|---|
jinshanmu/CrouzeixConjecture（GitHub ★169） |
✅ 真实 | 金山木公开的 Crouzeix 猜想候选证明工作区：LaTeX 手稿 + Annals 格式投稿稿 + 60+ 个 Lean 4 形式化文件 + 公理审计；仓库根目录的 crouzeix_conjecture_prompt.txt 即原始任务规格（本包已收录于 sources/） |
| arXiv:2607.20525（Yichen Huang, 2026-07-09） | ✅ 真实 | 《Autonomous disproofs of the sum-product conjecture over ℝ with GPT-5.5 Pro》：三阶段流水线 proof-plan proposal → proof construction → review；8 次独立运行 7 次正确、1 次自识别缺口；平均 13.24 万 reasoning tokens/次；代码开源于 github.com/yichenhuang/sum-product |
本包不提供"神 prompt"。真正值得复刻的是两者共有的研究组织结构： 多样化并行探索 → 主动反例攻击 → 独立审计 → 缺口台账 → 定向重开 → 形式化验证。
┌─────────────────────────────┐
│ 04 Research Manager (根) │
│ 方法族注册表 · 路线台账 │
│ 轮次调度 · 交叉授粉 · 终审 │
└──────────┬──────────────────┘
│ 每轮
┌───────────┬───────────┼───────────┬───────────┐
▼ ▼ ▼ ▼ ▼
┌──────────┐ ┌──────────┐ ┌──────────┐ ┌──────────┐ ┌──────────┐
│ 01 Explorer│ │ 01 Explorer│ │ 01 Explorer│ │ 02 Counter│ │ 03 Proof │
│ ×4–16 并行 │ │ 互相隔离 │ │ 不同方法族 │ │ example │ │ Auditor │
│ │ │ │ │ │ │ Hunter │ │ 逐行审计 │
└──────────┘ └──────────┘ └──────────┘ └──────────┘ └──────────┘
└──────────────┬──────────────┘ │ │
▼ ▼ ▼
workspace/routes/ counterexamples/ audits/
（路线隔离，互不可见） 攻击报告+证书 裁决+缺口清单
│
▼
┌─────────────────────────────────────────┐
│ 05 Formalizer（可选）：Lean 4 翻译 → lake │
│ build → 公理审计（先核对问题陈述！） │
└─────────────────────────────────────────┘
- 早期隔离：不告诉大多数 agent 当前受青睐的方向，防止全员收敛到同一个诱人但残缺的约化。
- 方法族注册表：按数学思想（而非措辞）给路线分组；大量收敛到一族时，把部分 explorer 重定向到未开发表述。
- 定理强度缺口 = 阻塞：路线卡在与原问题等强度的缺失引理时标记
BLOCKED，只有出现真正的新机制/新构造才重开。 - 对抗审计贯穿：每个候选证明都查 gap、条件化、手挥、等价陈述循环使用。
- 产出契约：agent 必须返回具体引理/构造/方程/反例（带证明）；拒绝状态报告、"模糊乐观"、"routine"声称。
- 返回标准：只有完整证明通过对抗终审才返回；reduction、partial、best-effort 一律不算完成。
cd ~/math-research-agent
export DEEPSEEK_API_KEY=sk-... # 不设也行：脚本会自动从 ~/.hermes/config.yaml 找到 deepseek key
# 热身：数值半径不等式（有标准证明，用于端到端验证流水线）
python3 scripts/run_pipeline.py --problem examples/starter_problem.md --explorers 4 --rounds 2
# 正式题：换 problem 文件即可
python3 scripts/run_pipeline.py --problem my_problem.md --explorers 8 --rounds 3 --model deepseek-reasoner --lean| 方式 | 命令 | 适合 |
|---|---|---|
| DeepSeek API（并行 N 路） | python3 scripts/run_pipeline.py ... |
便宜、可并行、可脚本化 |
| Codex CLI | scripts/run_codex.sh <problem.md> |
单 agent 深度探索（带工具/代码执行） |
| Claude Code | scripts/run_claude.sh <problem.md> |
Anthropic 系单 agent |
| 混合 | 探索用 DeepSeek 铺路，审计/形式化交给更强模型 | 预算充裕时的最优解 |
Huang 论文实测 ≈13.2 万 reasoning tokens/次/路线。4 路线 × 2 轮 ≈ 8 次调用 ≈ 100 万 tokens 量级：
| 模型 | 参考单价（以官方为准） | 4 路线×2 轮粗估 |
|---|---|---|
| deepseek-chat / v4-flash | 极低（约 ¥1–4 / 百万 token） | 几块钱 |
| deepseek-reasoner | 略高 | 十几到几十块 |
| GPT/Claude 旗舰 | 高 | 几十美元级 |
控制手段：--rounds、--explorers、--max-tokens；audit/hunter 阶段可用小模型。
- 金山木仓库：候选证明，计算 + 对抗审计未见具体错误，正式同行评审待定。
- 2026-08-04：Lorist & Schwenninger 声称给出 Crouzeix 猜想完整证明（arXiv:2608.03841）；已被独立仓库
ZestyWombat854/crouzeix-dilation-positivity指出其 Remark 2 存在 2×2 反例 → 结论存疑、悬而未决。 - 2026-08-05：OpenAI 声称推翻 Connes 刚性猜想，24 小时内被数学家 Nielsen 逐行审查 3.7 万行 Lean 4 后驳回——"AI 证对了每句话，但已与原猜想无关"（量子位报道）。
⚠️ 教训：形式化验证只能证明你定义的东西。 问题陈述核对（Formalizer 第一步）与对抗审计，比多烧 tokens 更重要。
~/math-research-agent/
├── README.md
├── prompts/ # 系统底座 + 五角色 prompt + 审计清单
├── scripts/ # DeepSeek 流水线 / Codex / Claude 运行器
├── workspace/ # 运行时产物（路线/反例/审计/台账/终稿）
├── examples/starter_problem.md
└── sources/ # 原始材料：金山木 prompt 原文、核验记录
本包配套 Hermes skill math-proof-agent（已安装）。之后学实分析、线性代数、概率论，甚至研究投资模型，直接加载同一套「探索—反驳—审稿—验证」组织法，不用每次重写 prompt。