Skip to content

MATH_TOOL_CATALOG.md

Latest commit

 

History

History
72 lines (66 loc) · 8.2 KB

MATH_TOOL_CATALOG.md

File metadata and controls

72 lines (66 loc) · 8.2 KB
Raw
id MATH-TOOL-CATALOG
type tooling
status current
owner engineering
created 2026-09-01
last_reviewed 2026-09-01
review_cycle P90D

数学工具族目录

本目录是公开仓的能力边界与证据上限，不是某台机器的安装清单。surveyed 只表示已分类； source_locked 只表示来源固定；installed、smoke_checked、evidence_capable 和 verifier_admitted 必须由对应的公开校验器和可复核产物支持。公开仓当前只把 SymPy 的有限 证据切片和 Lean fixture 的内核验证作为高等级入口；其余工具族不能越权进入证明或验证路由。

工具 canary 的 schema、runner 和测试逻辑可复用，但没有公开运行报告就不宣称运行时已安装； GPU、宿主机、容器、模型和凭据不属于本目录。结果仍需绑定 ProblemContract、Attempt、 Result 与 evidence receipt。

工具族 解释与说明
T01 · 算筹、算盘、对数表、机械计算器 surveyed / route=none；仅作公开调研分类；没有安装、运行或独立验证器准入声明。
T02 · FORTRAN、BLAS/LINPACK 传统 surveyed / route=none；仅作公开调研分类；没有安装、运行或独立验证器准入声明。
T03 · Logic Theorist、resolution、Davis–Putnam surveyed / route=none；仅作公开调研分类；没有安装、运行或独立验证器准入声明。
T04 · REDUCE、Macsyma/Maxima surveyed / route=none；仅作公开调研分类；没有安装、运行或独立验证器准入声明。
T05 · Automath、LCF、NQTHM surveyed / route=none；仅作公开调研分类；没有安装、运行或独立验证器准入声明。
T06 · Mizar、HOL、Isabelle、Coq/Rocq surveyed / route=none；仅作公开调研分类；没有安装、运行或独立验证器准入声明。
T07 · Maple、Mathematica surveyed / route=none；仅作公开调研分类；没有安装、运行或独立验证器准入声明。
T08 · PARI/GP、FLINT/Arb surveyed / route=none；仅作公开调研分类；没有安装、运行或独立验证器准入声明。
T09 · GAP surveyed / route=none；仅作公开调研分类；没有安装、运行或独立验证器准入声明。
T10 · Singular、Macaulay2 surveyed / route=none；仅作公开调研分类；没有安装、运行或独立验证器准入声明。
T11 · SageMath surveyed / route=none；仅作公开调研分类；没有安装、运行或独立验证器准入声明。
T12 · SymPy evidence_capable / route=evidence；公开仓准入 evidence_capable；只覆盖固定 SymPy 精确算术/符号 vertical slice，不能替代通用证明器。
T13 · mpmath、python-flint surveyed / route=none；公开仓仅发布 surveyed 分类和有界 canary 契约；没有公开运行报告，不提供 runtime route。
T14 · NumPy、SciPy、Julia surveyed / route=none；仅作公开调研分类；没有安装、运行或独立验证器准入声明。
T15 · Z3、cvc5、SMT-LIB surveyed / route=none；公开仓仅发布 surveyed 分类和有界 canary 契约；没有公开运行报告，不提供 runtime route。
T16 · MiniSat、CaDiCaL surveyed / route=none；公开仓仅发布 surveyed 分类和有界 canary 契约；没有公开运行报告，不提供 runtime route。
T17 · E、Vampire、Prover9、TPTP surveyed / route=none；仅作公开调研分类；没有安装、运行或独立验证器准入声明。
T18 · Lean 4/Mathlib verifier_admitted / route=verifier；公开仓准入 verifier_admitted；只覆盖固定 Lean/Mathlib fixture 的 kernel、axiom 与 faithfulness 门。
T19 · HOL Light、Isabelle、Rocq、Metamath、ACL2 surveyed / route=none；仅作公开调研分类；没有安装、运行或独立验证器准入声明。
T20 · polymake、4ti2、TOPCOM surveyed / route=none；仅作公开调研分类；没有安装、运行或独立验证器准入声明。
T21 · nauty/Traces、NetworkX、igraph surveyed / route=none；仅作公开调研分类；没有安装、运行或独立验证器准入声明。
T22 · OEIS、LMFDB、DLMF、TPTP surveyed / route=none；仅作公开调研分类；没有安装、运行或独立验证器准入声明。
T23 · Gappa、区间算术与浮点证书 surveyed / route=none；仅作公开调研分类；没有安装、运行或独立验证器准入声明。
T24 · Alethe/Eunoia、CPC、Carcara、SMTCoq source_locked / route=none；仅作公开调研分类；没有安装、运行或独立验证器准入声明。
T25 · Isabelle/HOL + LLM prover（Isabellm） surveyed / route=none；仅作公开调研分类；没有安装、运行或独立验证器准入声明。
T26 · OpenTheory / proof exchange packages source_locked / route=none；仅作公开调研分类；没有安装、运行或独立验证器准入声明。
T27 · LeanDojo-v2 / TorchLean / ITPEval 生态 source_locked / route=none；仅作公开调研分类；没有安装、运行或独立验证器准入声明。
T28 · Axiom / FriCAS surveyed / route=none；仅作公开调研分类；没有安装、运行或独立验证器准入声明。
T29 · Macaulay2 / Singular surveyed / route=none；仅作公开调研分类；没有安装、运行或独立验证器准入声明。
T30 · GAP / SageMath surveyed / route=none；仅作公开调研分类；没有安装、运行或独立验证器准入声明。
T31 · ACL2 / TPTP-SZS surveyed / route=none；仅作公开调研分类；没有安装、运行或独立验证器准入声明。
T32 · FLINT / Arb surveyed / route=none；仅作公开调研分类；没有安装、运行或独立验证器准入声明。
T33 · OSCAR.jl surveyed / route=none；仅作公开调研分类；没有安装、运行或独立验证器准入声明。
T34 · Dedukti source_locked / route=none；仅作公开调研分类；没有安装、运行或独立验证器准入声明。
T35 · Agda surveyed / route=none；仅作公开调研分类；没有安装、运行或独立验证器准入声明。
T36 · LFSC surveyed / route=none；仅作公开调研分类；没有安装、运行或独立验证器准入声明。
T37 · PVS surveyed / route=none；仅作公开调研分类；没有安装、运行或独立验证器准入声明。
T38 · Nuprl / MetaPRL surveyed / route=none；仅作公开调研分类；没有安装、运行或独立验证器准入声明。
T39 · Maude surveyed / route=none；仅作公开调研分类；没有安装、运行或独立验证器准入声明。
T40 · OpenMath surveyed / route=none；仅作公开调研分类；没有安装、运行或独立验证器准入声明。
T41 · SMT-LIB / SMT-LIB-db surveyed / route=none；仅作公开调研分类；没有安装、运行或独立验证器准入声明。

可复核入口

  • 能力分类：governance/control-plane/math-tool-maturity.v1.json。
  • 结构校验：scripts/validate_math_tool_maturity.py。
  • 可移植测试：scripts/test_validate_math_tool_maturity.py、scripts/test_check_math_tools.py。
  • 受限 canary：scripts/run_math_tool_canaries.py；只在显式配置的运行时中执行，所有子进程有 timeout，输出不进入研究记录。
  • 证据上限：有限数值/符号输出只能支持对应切片；kernel_check 仍不替代自然语言陈述忠实性审查。