math-rigor

DeepSeek Harness (DSH) 插件生态允许通过本地工具和脚本扩展智能体的能力。math-rigor 插件针对数学证明场景，通过本地 MCP 服务器和结构化工作流，提供可审计的证明过程，避免模型直接“幻觉”出结论。

核心组件¶

该插件由三部分组成：

本地 stdio MCP 服务器：运行 Python 脚本，提供 23 个工具。
Bundled workflow skill：内置证明流程 skill。
Slash commands：提供 /prove 和 /audit-proof 两个命令。

安装与启用¶

使用官方提供的安装命令添加插件。请根据你当前使用的 profile 修改命令中的 --profile 参数（例如 desktop 或 web）。

dsh plugin --profile web add bauerelizabeth07139/math-rigor

安装完成后，插件会注册相应的 skill 和命令。在首次使用前，需要确保 Python 环境已准备就绪。

环境要求¶

该插件依赖 Python 3.10+。MCP 工具在虚拟环境（venv）创建并安装依赖之前不可用。

安装依赖：插件需要 mcp、sympy、z3-solver 和 mpmath。
环境路径：所有数据（包括 venv 和证明会话）默认存储在 $DSH_HOME/math-rigor。

如果环境未就绪，MCP 工具将不可用，命令会返回错误并提示需要执行 setup 脚本或手动创建 venv。

配置¶

在 profile 的 loader row 中配置插件参数：

- id: dsh-math-rigor
  config:
    home: "$DSH_HOME/math-rigor"
    setup: true
    setupTimeoutMs: 600000
    toolCallTimeoutMs: 300000

配置项说明：
* home：指定数据目录，默认为 $DSH_HOME/math-rigor。
* setup：布尔值。设为 true 时，插件会在加载阶段自动创建 venv 并安装依赖。
* setupTimeoutMs / toolCallTimeoutMs：设置安装和工具调用的超时时间（毫秒）。

使用命令¶

插件提供了两个主要命令：

/prove <mathematical proposition>
- 启动一个六阶段的严格证明工作流：形式化 → 策略 → 引理分解 → 逐步证明（每步机检）→ 机器审计 → 报告。
- 前置条件：必须在执行前加载 math-rigor skill。
/audit-proof <proof text or math-rigor session id>
- 对证明文本或会话 ID 进行审查。它会拆解步骤 DAG，逐条读取判定结果，并进行结构性审查，列出问题清单。

23 个 MCP 工具¶

MCP 工具以 mcp__math_rigor__ 为前缀。工具分为五组：

会话管理¶

proof_workflow：返回流程阶段、判定词汇表与审计检查项。
proof_start：开始一个证明会话，登记问题、目标和符号定义域。
proof_add_given：登记题面给定的前提。
proof_add_assumption：登记临时假设。
proof_add_lemma：登记引理义务。
proof_add_step：添加证明步骤并立即机检。
proof_validate：审计整个证明结构。
proof_status：查看会话状态。
proof_export：导出证明为 Markdown / LaTeX / JSON。

逻辑检查¶

logic_check_step：检查单步推理的形状和语义。
logic_entails：判断前提是否蕴含结论。
logic_truth_table：纯命题逻辑完全枚举（最多 10 变量）。
logic_rules：列出推理规则。

验证器¶

verify_identity：验证两个表达式是否为同一函数。
verify_inequality：验证带定义域的全局不等式。
verify_forall：验证全称命题（整除、奇偶、界、代数恒等式）。
verify_induction：验证归纳法。
verify_limit：验证极限值。
find_counterexample：寻找反例。

符号运算¶

symbolic_eval：单次符号运算（simplify, expand, factor, diff, integrate 等）。
symbolic_numeric：高精度数值求值。
expr_normalise：规范化表达式。

数论¶

number_theory：精确整数运算（质数、因数分解、欧拉函数、GCD、CRT 等）。

安全性¶

该插件在安全性上做了严格限制：

输入隔离：输入仅为数学表达式，不使用 eval 或 exec 执行任意代码。输入经过词法/语法分析器解析成 AST。
文件操作：仅写入插件家目录（$DSH_HOME/math-rigor），不写入工作目录或 profile 配置。
网络隔离：仅在初始 pip install 时使用网络，证明过程完全离线。
依赖锁定：requirements.txt 中的依赖版本被严格锁定。

总结¶

math-rigor 为 DSH 提供了一套从输入到验证、再到审计的完整数学证明工具链。它通过 23 个本地工具和结构化的 /prove 工作流，确保了数学推理的可信度。

插件主页：https://www.skillhub.cn/plugins/bauerelizabeth07139/math-rigor
源码仓库：https://github.com/bauerelizabeth07139/math-rigor