# Derstedtcasper Mathprove Skill Skill

> MathProve Skill

- Skill: `tomevault-io/derstedtcasper-mathprove-skill-skill` (Agent Skill, multi-file: 2 files)
- Install (CLI): `npx skillmds@latest add tomevault-io/derstedtcasper-mathprove-skill-skill`
- Raw SKILL.md: https://api.skillmd.com/api/skills/tomevault-io/derstedtcasper-mathprove-skill-skill/raw
- Safety review: pending (external: skill-scanner PASS, skillspector PASS)
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: Coding & Dev Tools
- Author: tomevault-io (https://skillmd.com/u/tomevault-io)
- Updated: 2026-09-17
- Page: https://skillmd.com/skills/tomevault-io/derstedtcasper-mathprove-skill-skill

---


# 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](https://tomevault.io/claim/derstedtcasper) — claim your Tome and manage your conversions.
<!-- tomevault:4.0:skill_md:2026-04-13 -->