Skip to content

Releases

math-rigor v1.1.0

Choose a tag to compare

@bauerelizabeth07139 bauerelizabeth07139 released this 17 Sep 01:06

✨ v1.1.0 更新

  • README 全面升级:新增 ASCII 英雄横幅、判定状态机(Mermaid stateDiagram)、目录导航、/prove 与 /audit-proof 的 kbd 快捷键、数据统计条与全新徽章行。

🧩 功能一览

  • 23 个 MCP 工具的严格数学证明服务器(sympy + z3 双引擎,残数分情形 / 存在式改写补强数论判定)
  • 六阶段证明工作流 + 三级审计判定(verified / sound_with_gaps / flawed),判定词汇永不混淆(proven / refuted / inconclusive)
  • /prove 与 /audit-proof slash 命令,Windows / macOS / Linux 一键安装脚本
  • CI:3 系统 × 2 Python 版本冒烟测试 + 全量测试(8 模块 / 275 断言)

源码归档由 GitHub 自动生成(Source code zip / tar.gz)。

math-rigor v1.0.0

Choose a tag to compare

@bauerelizabeth07139 bauerelizabeth07139 released this 16 Sep 17:41

∷ math-rigor v1.0.0

在 ZCode 上进行严格、可审计的数学证明:本地 MCP 服务器(23 个工具)+ 流程 skill + 两个 slash 命令。

核心设计

  • 判定词汇只有三种,永不混淆:proven(否定式不可满足)/ refuted(给出具体反例)/ inconclusive(不是证明)。
  • 审计分三级:verified / sound_with_gaps(有步骤依赖人工论证,必须披露)/ flawed。
  • 推理规则双重检查:22 条规则先验形状、再验语义;universal_generalization 与 existential_instantiation 明确标注语义不自足并改验新鲜性。
  • 代数步骤被重新推导:algebra 步骤从其引用的前提重推,推不出即 refuted 并附反例。
  • 让 SMT 真能证出数论命题:残数分情形 + ∃k: A = c·k + d 自动改写为 c | (A−d),6 | n³−n、30 | n⁵−n 可直接判定。

工具(23 个)

  • 证明会话:proof_start / proof_add_given / proof_add_assumption / proof_add_lemma / proof_add_step / proof_validate / proof_status / proof_export / proof_workflow
  • 逻辑:logic_check_step / logic_entails / logic_truth_table / logic_rules
  • 数学:verify_identity / verify_inequality / verify_forall / verify_induction / verify_limit / find_counterexample / symbolic_eval / symbolic_numeric / number_theory / expr_normalise

安装

git clone https://github.com/bauerelizabeth07139/math-rigor.git
cd math-rigor
powershell -ExecutionPolicy Bypass -File .\install.ps1   # 或 ./install.sh

需要 Python 3.10+。安装脚本会先验证服务器能起来,再修改你的 ZCode 配置。

质量

  • 8 个测试模块、约 275 条断言,含真实 MCP stdio 协议端到端(23 个工具逐一调用并断言)。
  • CI:GitHub Actions 在 3 个系统 × 2 个 Python 版本上全绿。
  • references/inference-rules.md 与 references/worked-examples.md 由代码与真实工具返回生成,与实现保持一致。