mathprove

by @DerstedtCasper in AI & LLM

# Install this skill:

npx skills add DerstedtCasper/MathProve-Skill

Or install specific skill: npx add-skill https://github.com/DerstedtCasper/MathProve-Skill

# Description

组合式数学推导与证明技能。适用于需要分步拆解、难度评估、在 SymPy 与 Lean4+Mathlib 间灵活切换、逐步验证并生成可审计草稿与正式稿的数学问题；可选启用 subagent 路由进行并行化解释/引理检索/证明骨架构建。

# SKILL.md

name: mathprove
description: 组合式数学推导与证明技能。适用于需要分步拆解、难度评估、在 SymPy 与 Lean4+Mathlib 间灵活切换、逐步验证并生成可审计草稿与正式稿的数学问题；可选启用 subagent 路由进行并行化解释/引理检索/证明骨架构建。

MathProve（分步验证 + 路由 + 子代理 + 严格复核）

目标

把数学问题拆成最小可验证步骤（step），对每一步进行难度评估并选择 SymPy 或 Lean4 路线；每一步通过后写入 draft.md；最终对所有步骤做一致性复核（可选启用 Lean4 reverse gate）并生成 Solution.md。

快速开始

环境检查（推荐验证 Mathlib）：
python scripts/check_env.py --project "D:\MATH Studio\math_studio" --verify-mathlib
生成步骤清单（JSON）：
结构见 assets/step_schema.json
step id 强烈推荐使用 S1/S2/...（与 Lean theorem/lemma 名称对齐）
问题级路由（含 subagent 建议）：
python scripts/problem_router.py --text "<问题>"
步骤级路由（难度与路线建议）：
python scripts/step_router.py --input steps.json --output steps.routed.json --explain
（可选）生成子代理任务包（并行解释/引理检索/证明骨架）：
python scripts/subagent_tasks.py --steps steps.routed.json --out-dir subagent_tasks --emit-md
每步验证通过后写入草稿：
python scripts/draft_logger.py --draft draft.md --step-file one_step.json
最终复核并生成正式稿（可选启用 Lean4 reverse gate）：
python scripts/final_audit.py --steps steps.routed.json --solution Solution.md --lean-cwd "D:\MATH Studio\math_studio" --lean-gate

核心流程（必须遵守）

Problem Lock（问题锁定）
在推导前写清：目标结论、变量域/类型、允许使用的已知结果、成功标准。
Notation + Assumptions（符号与假设）
先写 符号表/假设台账（模板见 assets/templates/notation_table.md、assets/templates/assumption_ledger.md）。
Step 拆解
每个 step 只做一个可校验的“子目标”。
难度评估与路线选择
easy 且可符号化：优先 SymPy。
medium/hard 或需要形式化保证：Lean4+Mathlib。
思路不清晰/开放性：允许联网启发（只取灵感），再用 Lean4 反推验证。
工具校验（必须通过才可写入草稿）
SymPy：scripts/verify_sympy.py
Lean4：scripts/lean_repl_client.py（优先 repl；无 repl 时用 file/auto）
草稿记录（演讲友好）
每步写入 draft.md 时，必须补齐：符号/假设/讲解版解释（否则答辩/讲座容易被打断）。
最终复核（禁止口头保证）
scripts/final_audit.py 会逐步回放校验结果，全部通过才生成 Solution.md。

Step 数据契约（强约束，提升可校验性）

step id：推荐 S1/S2/...（用于映射 Lean theorem/lemma 名称）。
对于 checker.type = sympy：
使用 checker.code 或 checker.code_file，并写清 symbols/assumptions/explanation。
对于 checker.type = lean4：
使用 checker.cmds（或 checker.code 作为逐行片段）。
必须包含 theorem/lemma Sx ... := by ...，且 x 与 step id 一致。

Subagent 路由（可选，推荐用于难题/长证明）

适用：步骤较多、需要大量讲解、需要检索 Mathlib 引理、或 Lean4 证明较难时。

角色分工建议：
- 主 agent：拆步、确定目标与依赖、汇总回填 steps.json/draft/Solution。
- 子代理：逐 step 输出
- 讲解版解释（符号定义/关键不变量/逻辑跳跃）
- Mathlib lemma 候选与使用方式（可直接 apply/have）
- SymPy 验证片段（最小可运行 + 期望结果）
- Lean4 证明骨架（避免 sorry/admit）

启用方式（保守探测 + 显式开关）：
- 显式：设置 MATHPROVE_SUBAGENT=1（可选 MATHPROVE_SUBAGENT_DRIVER）
- 生成任务包：scripts/subagent_tasks.py

如果运行环境不支持 subagent：任务包仍可当作“自检清单”顺序执行（流程不变）。

Lean4 reverse gate（强烈推荐）

用途：把 Lean4 证明从“单步运行 OK”升级为“统一严格门禁”：
- 自动生成 reverse_gate.lean
- 运行 lint：禁止 sorry/admit/axiom/constant/opaque，要求 step map
- 用 lake env lean 编译通过（默认要求 Mathlib/Lake 工程；除非显式 --lean-gate-no-mathlib）

入口：
- python scripts/final_audit.py ... --lean-gate
- 也可手动：scripts/check_reverse_lean4.ps1 -Path <lean> -ProjectDir <lake-root> -RequireMathlib -RequireStepMap

联网启发记录

联网检索只用于启发思路；任何外部信息必须记录来源摘要并再回证：
- 记录脚本：scripts/web_inspiration.py
- 示例：references/web-inspiration-example.md

模板化流程（讲解友好）

assets/templates/ 提供可复用结构，建议在草稿/正式稿中保持一致：
- draft_template.md / solution_template.md / audit_template.md
- notation_table.md / assumption_ledger.md
- claim_list.md / claim_evidence_matrix.md
- （可选深度）baseline_evidence.md / competing_models.md / red_team_review.md / validation_plan.md / sympy_checklist.md

错误处理（必须执行）

SymPy/Lean4 单步失败：先分析错误原因，再有限重试（不超过 3 次）。
若仍失败：将 step 标记为失败，停止进入最终复核（不得生成正式稿）。
禁止在未验证通过的情况下写入草稿或生成正式稿。

资源与参考

脚本
- scripts/verify_sympy.py：执行 SymPy 校验
- scripts/lean_repl_client.py：Lean4（repl/file/auto）执行
- scripts/final_audit.py：最终复核 + 生成 Solution.md
- scripts/lint_reverse_lean4.py：Lean4 reverse gate lint
- scripts/check_reverse_lean4.ps1：Lean4 reverse gate（lint + 编译）
- scripts/subagent_tasks.py：生成子代理任务包

关键资源
- assets/step_schema.json
- assets/lean/reverse_template_mathlib.lean

# README.md

MathProve

MathProve 是一个神经符号（Neuro-Symbolic）数学验证流水线。通过集成符号计算引擎（SymPy）与交互式定理证明器（Lean 4），为大语言模型（LLM）的数学推理过程提供形式化验证与可追溯审计。

本项目聚焦于 LLM 在数学推导中的“幻觉”现象：将 Chain-of-Thought (CoT) 映射为可执行代码或形式化命题，确保最终生成的 Solution.md 中每一步都经过计算验证或逻辑检查。

核心特性

混合求解路由 (Hybrid Routing)：自动分析推理步骤属性；计算类任务分发至 SymPy；逻辑证明类任务分发至 Lean 4 + Mathlib。
严格门禁机制 (Strict Gatekeeping)：仅通过执行引擎校验的步骤（Step）可合并至最终解；失败步骤触发回滚或重试。
形式化审计 (Formal Auditing)：支持生成完整 .lean 源文件并调用编译器进行全局一致性检查，杜绝滥用 sorry 或循环论证。
结构化输出：生成包含符号定义、假设前提及验证状态的标准化 Markdown 文档。

架构概览

MathProve 的工作流包含以下阶段：

Decomposition：将自然语言问题拆解为原子化 steps.json。
Routing & Execution：
CAS Track：调用 Python/SymPy 进行代数运算、微积分求解等计算验证。
ITP Track：构造 Lean 4 命题，利用 Mathlib 策略库（tactics）完成证明。
Verification：验证每一步的返回状态、标准输出与期望结果。
Synthesis：聚合所有通过的步骤，生成最终报告（draft.md → Solution.md）。

环境依赖

Python 3.8+
Lean 4 + Lake（用于形式化验证；需可在 PATH 中调用，或显式提供可执行路径）
Python 依赖：

python -m pip install -r requirements-dev.txt

安装

作为独立 CLI 工具使用

git clone https://github.com/DerstedtCasper/MathProve-Skill.git MathProve
cd MathProve

集成到 Agent/Codex（可选）

建议以软链接/目录联接方式挂载到 Codex skills 目录（Windows 默认 %USERPROFILE%\.codex\skills\）：

New-Item -ItemType Junction `
  -Path "$env:USERPROFILE\.codex\skills\MathProve" `
  -Target "D:\AI bot\MathProve"

快速开始

1) 环境自检（推荐）

在运行复杂证明前，确保 Lean 4 工程路径可用且 Mathlib 已编译：

python scripts/check_env.py --project "<path-to-lean-project>" --verify-mathlib

2) 标准工作流（CLI）

步骤 A：路由与单步验证

python scripts/step_router.py \
  --input "steps.json" \
  --output "steps.routed.json" \
  --explain

参数说明：

--explain：在日志中输出路由决策理由（SymPy vs Lean）

步骤 B：全局审计与生成

python scripts/final_audit.py \
  --steps "steps.routed.json" \
  --solution "Solution.md" \
  --lean-cwd "<path-to-lean-project>" \
  --lean-gate

参数说明：

--lean-gate：启用严格模式，生成 reverse_gate.lean 并调用 Lean 编译器验证整条推导链

输入数据格式示例

steps.json 的结构以 assets/step_schema.json 为准。以下示例展示常见的 SymPy 步骤与 Lean4 步骤：

{
  "problem": "证明并验证：对任意实数 x，有 (x+1)^2 = x^2 + 2x + 1",
  "steps": [
    {
      "id": "S1",
      "goal": "展开 (x + 1)^2",
      "checker": {
        "type": "sympy",
        "code": "import sympy as sp\nx = sp.Symbol('x')\nexpr = (x + 1)**2\nassert sp.expand(expr) == x**2 + 2*x + 1\nprint('ok')"
      }
    },
    {
      "id": "S2",
      "goal": "形式化：Nat 加法右单位元",
      "checker": {
        "type": "lean4",
        "cmds": [
          "import Mathlib",
          "theorem S2 (n : Nat) : n + 0 = n := by simp"
        ]
      }
    }
  ]
}

高级配置

Lean Reverse Gate（反向验证）

为防止生成“语法正确但逻辑无效”的证明（例如滥用 axiom、constant 或 sorry），可启用 reverse gate 进行全局门禁：

生成 reverse_gate.lean 并聚合所有 Lean step
lint：禁止 sorry/admit/axiom/constant/opaque 等捷径
在 Lake 工程中执行 lake env lean reverse_gate.lean 进行编译级校验

Windows 下可直接运行：

pwsh -File scripts/check_reverse_lean4.ps1 `
  -Path "reverse_gate.lean" `
  -ProjectDir "<path-to-lean-project>" `
  -RequireMathlib `
  -RequireStepMap

Subagent 并行化

对长链推导任务，可通过环境变量开启子任务拆分模式，并生成可分发任务包：

export MATHPROVE_SUBAGENT="1"
python scripts/subagent_tasks.py --steps steps.routed.json --out-dir ./tasks

目录结构

scripts/：核心逻辑脚本
step_router.py：步骤分发器（SymPy vs Lean4）
final_audit.py：最终审计与 Solution.md 生成
check_reverse_lean4.ps1：reverse gate（lint + 编译）
assets/：schema 与模板（含 assets/step_schema.json、assets/templates/）
tests/：单元测试

License

MIT License

# Supported AI Coding Agents

This skill is compatible with the SKILL.md standard and works with all major AI coding agents:

⚡ Amp 🚀 Antigravity 🤖 Claude Code 🦀 Clawdbot 📝 Codex ▶️ Cursor 🤖 Droid 💎 Gemini CLI 🐙 GitHub Copilot 🪿 Goose 📊 Kilo Code 🔧 Kiro CLI 💻 OpenCode 🦘 Roo Code 🌲 Trae 🏄 Windsurf

Learn more about the SKILL.md standard and how to use these skills with your preferred AI coding agent.

mathprove

# Description

# SKILL.md

MathProve（分步验证 + 路由 + 子代理 + 严格复核）

目标

快速开始

核心流程（必须遵守）

Step 数据契约（强约束，提升可校验性）

Subagent 路由（可选，推荐用于难题/长证明）

Lean4 reverse gate（强烈推荐）

联网启发记录

模板化流程（讲解友好）

错误处理（必须执行）

资源与参考

# README.md

MathProve

核心特性

架构概览

环境依赖

安装

作为独立 CLI 工具使用

集成到 Agent/Codex（可选）

快速开始

1) 环境自检（推荐）

2) 标准工作流（CLI）

输入数据格式示例

高级配置

Lean Reverse Gate（反向验证）

Subagent 并行化

目录结构

License

# Related Skills

# Supported AI Coding Agents

Confirm

Submit a Skill