mathprove-skill

name	mathprove-skill
description	| Use when this capability is needed.

MathProve Skill

本技能把证明当成可执行、可复核的软件流水线。每个结论必须绑定物理证据。

---

0. 不可谈判硬规则（MUST）

0.1 目录写入边界 — 只能在 WORKSPACE/ 下读写产物。禁止在 skill 包内写入任何临时文件。

0.2 禁止角色扮演 — 不得在主线程假装三人格。MAGI 必须通过 scripts/magi_plan.py 实现。

0.3 门控写入 — 仅当 MAGI=APPROVED + SymPy 通过 + Lean4 通过 + 证据包齐全，才允许写入 draft 并标记 passed。

0.4 终局约束 — final_audit.py 输出 APPROVED 之前，不得宣称"证明完成"。

0.5 可复核 — 每次工具调用的命令、输入、输出、退出码，必须落盘 workspace。

---

1. 工作区结构

WORKSPACE/runs/<run_id>/
├── problem.md / assumptions.md / manifest.json / status.json
├── plan/        steps.json + steps_readme.md
├── magi/        step_XXX_vote.json
├── sympy/       step_XXX_check.py + step_XXX_out.txt
├── lean/        StepXXX.lean + step_XXX_lean.log
├── draft/       step_XXX.md + proof_draft.md
├── evidence/    step_XXX_evidence.json
├── audit/       audit.json + Solution.md + FAILURE_REPORT.md
└── logs/        init_check.log + tool_calls.log + errors.log

run_id 格式：YYYYMMDD_HHMMSS_<short_hash>

---

2. 强制流程（4 阶段）

阶段	步骤	详细 SOP
A. 预检	check_routes → 创建 run 目录 → 写 problem.md + assumptions.md	—
B. 规划	magi_plan → steps.json → 结构校验	—
C. 逐步循环	对每个 step: proposal → MAGI → SymPy → Lean4 → evidence → draft	sop/magi.md sop/sympy.md sop/lean.md sop/evidence.md
D. 审计	final_audit → audit.json + Solution.md	sop/audit.md

失败时参考 sop/error.md。

---

3. steps.json 最小 Schema

每个 step 必须原子化（一次只做一个可验证的最小推导单元），包含：

• id, title, claim（含 LaTeX）
• inputs（前置 step id 列表）
• method（sympy/lean/both）
• sympy: { required, check_goal }
• lean: { required, theorem_goal }
• evidence_required, risks, accept_criteria

---

4. status.json 状态机

phase: init → planning → step_loop → auditing → done | failed
step.status: pending → magi_approved → sympy_passed → lean_passed → passed | failed

使用 ProofSearchTree 管理，非法转移抛 ValueError。详见 sop/runtime.md。

---

5. 运行时模块（v1.0）

模块	路径	职责
ProofSearchTree	runtime/proof_tree.py	状态机管理
ErrorClassifier	runtime/error_classifier.py	三级错误分类 + RetryBudget
ParallelRunner	runtime/parallel_runner.py	N 分支并行竞速
SafeVerify	runtime/safe_verify.py	Lean4 白盒审计
Orchestrator	runtime/orchestrator.py	一键编排入口

详细 API 参考 sop/runtime.md。

---

6. SOP 按需加载索引

SOP 文件	加载时机
sop/magi.md	阶段 C — 每个 step 验证前
sop/sympy.md	阶段 C — MAGI 通过后 SymPy 验证
sop/lean.md	阶段 C — SymPy 通过后 Lean4 验证
sop/evidence.md	阶段 C — 验证全部通过后写证据+草稿
sop/audit.md	阶段 D — 终局审计
sop/error.md	任何验证失败时
sop/runtime.md	需要 Runtime API 参考时

---

7. 汇报规范

• 每次汇报含：run_id、当前 phase/step、通过/失败、证据路径
• 不贴长日志全文（最多 5~20 行关键错误行）
• 完整日志留在 workspace，指向文件路径

---

8. 执行清单

• check_routes 成功 + logs/init_check.log
• run 目录 + problem.md + assumptions.md + status.json
• steps.json 每步有 evidence_required + accept_criteria
• 每步：MAGI vote → SymPy PASS → Lean4 PASS → evidence → draft
• final_audit = APPROVED → 输出 Solution.md

---

Converted and distributed by TomeVault — claim your Tome and manage your conversions.