⚙️

math-rigor

工作流更新于 2026.10.08

在终端中运行以下命令：

dsh plugin install bauerelizabeth07139/math-rigor

将以下提示词粘贴到 DeepSeek Harness 对话框中：

在 DeepSeek Harness 中可用 CLI 执行 dsh plugin install bauerelizabeth07139/math-rigor，或在 Desktop 的 Plugins → Add plugin 填入 https://github.com/bauerelizabeth07139/math-rigor 并启用对应 bundle。

插件介绍

在对话式 Agent 里做数学证明，常见痛点是「看起来像证明」与「每一步都被机器核对」混在一起：求解器没定论就被说成证成了，反例找到了却和「不可满足」共用同一套话术。math-rigor 作为 DSH 0.2.x 的 Cordis 宿主插件，把可审计的严格证明收进一条本地工具链——隔离 Python 环境经 stdio 启动 MCP 服务器，向 Agent 暴露 23 个以 mcp__math_rigor__ 为前缀的工具，并配套 bundled math-rigor skill 与 /prove、/audit-proof 两条斜杠命令。

设计上只坚持一件事：判定词汇不混用。证明侧区分 proven（否定式不可满足）、refuted（有反例）、inconclusive（未决定且无反例，明确不是证明）；审计侧区分 verified、sound_with_gaps（结构成立但有未检步骤）、flawed（存在被推翻或无效步骤等）。/prove 排入六阶段流程——形式化、策略、引理分解、逐步机检、机器审计、如实报告；/audit-proof 则做步骤 DAG 审查与问题清单。工具覆盖证明会话管理、逻辑推理与真值表、恒等式/不等式/全称/归纳/极限验证、反例搜索、符号运算与数论等，输入经 AST 解析而非 eval，证明过程本身可离线运行。

适合在 DeepSeek Harness 里需要写推导、验恒等式或不等式、做归纳或整除论证、主动找反例，或审查既有证明是否每一步站得住的用户与 Agent 工作流。环境未就绪时 skill 与命令仍可注册，但 MCP 工具与两条命令会明确报错并提示如何建 venv，避免在工具缺席时静默胡编证明。