dsh-math-rigor: 本地可審計的數學證明工具鏈

DeepSeek Harness (DSH) 採用插件化架構。在模型推理任務中，特別是數學證明場景，驗證 AI 生成的推導過程往往依賴人工檢查。dsh-math-rigor 插件通過本地 MCP 服務器將形式化證明工具鏈接入 DSH，提供可審計的證明流程和自動化驗證能力。

插件定位¶

這是一個運行在 DSH 0.2.x 上的 Cordis host plugin。它包含一個本地 stdio MCP 服務器（提供 23 個工具）、一個內置的 math-rigor skill 以及兩個 slash 命令（/prove 和 /audit-proof）。其核心價值在於將形式化證明流程引入智能體工作流，確保數學推導的可信度。

核心功能¶

插件主要包含以下能力：

本地 MCP 服務器：通過 stdio 協議與 DSH 通信，提供 23 個工具用於處理證明、符號計算和邏輯檢查。
內置 Skill：math-rigor skill 處理證明、推導、恆等式驗證、歸納法及反例搜索等任務。
Slash 命令：
- /prove <命題>：自動執行形式化、策略制定、引理分解、逐步機檢、機器審計、最終報告的六階段流程。
- /audit-proof <文本或會話 ID>：對證明文本或會話進行審查，拆解步驟 DAG、讀取判定結果、進行結構性檢查並生成問題清單。

安裝與啓用¶

使用 CLI 安裝插件（需指定 profile）：

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

若機器上未安裝 git，可使用 tarball 地址：

dsh plugin --profile web add https://codeload.github.com/bauerelizabeth07139/dsh-math-rigor/tar.gz/main

前置條件與配置¶

插件依賴 Python 3.10+ 及 mcp、sympy、z3-solver、mpmath。

首次加載時必須配置 setup: true 或運行 tools/setup_dsh.py 來建立虛擬環境並安裝依賴。環境就緒前，MCP 工具不可用。證明過程完全離線（僅安裝期間使用網絡）。

配置項示例（在 profile 的 loader row 中）：

- id: dsh-math-rigor
  config:
    home: "D:/math-rigor-data"
    setup: true

適用場景與安全機制¶

適用場景：需要高可信度數學推導、形式化驗證、符號計算及邏輯推理的 DSH 智能體開發。
安全機制：插件在安全設計上嚴格限制輸入，不使用 eval 執行用戶輸入，不執行 shell 命令，不進行文件寫入（除插件 home 目錄外），且無網絡連接用於推理。

總結¶

dsh-math-rigor 爲 DSH 生態提供了嚴謹的數學證明基礎設施。通過將工具鏈下沉到本地，它確保了證明過程的透明性與可審計性。更多詳情可查看插件目錄或 GitHub 倉庫。