用途
math-help 是 continuous-claude-v3 项目中的数学认知栈（Math Cognitive Stack）指南，定位为“精确数学计算的认知假体”。它的核心作用是帮助用户在面对数学任务时，判断应当使用哪一层工具，并给出对应的命令示例。
主要能力
该指南将数学工具划分为五个层次：
- SymPy（符号代数）：用于精确的代数计算，包括解方程、积分、微分、化简、求极限、矩阵特征值等。适合需要闭式解、微积分和精确代数的场景。
- Z3（约束求解与定理证明）：用于证明定理、检查可满足性、带约束的优化。适合逻辑证明、约束满足和约束优化问题。
- Math Scratchpad（推理验证）：用于验证逐步推理、检查推导链、解释单个步骤。适合检查自己的解题过程、验证推导。
- Math Tutor（教育）：用于学习、获取提示、生成练习题，提供分步解答。适合学习、辅导和练习。
- Lean 4（形式化证明）：用于严格的机器验证数学证明、范畴论、类型论。适合发表级证明、依赖类型和范畴论。
此外还包含数值工具：NumPy（160 个函数，矩阵运算、线性方程组）、SciPy（289 个函数，最小化、求根、曲线拟合）、mpmath（153 个函数，任意精度计算），以及可视化工具 math_plot.py（二维图、三维曲面、多函数图、LaTeX 渲染）。
使用方式
指南以快速参考表的形式列出常见需求与对应命令，例如：解方程使用 sympy_compute.py solve，积分/微分使用 sympy_compute.py，求极限使用 sympy_compute.py limit，矩阵运算使用 sympy_compute.py 或 numpy_compute.py，验证推理步骤使用 math_scratchpad.py verify，检查证明链使用 math_scratchpad.py chain，获取渐进提示使用 math_tutor.py hint，生成练习题使用 math_tutor.py generate，证明定理使用 z3_solve.py prove，检查可满足性使用 z3_solve.py sat，约束优化使用 z3_solve.py optimize，绘图使用 math_plot.py，任意精度使用 mpmath_compute.py，数值优化使用 scipy_compute.py，形式化机器证明使用 Lean 4（lean4 skill）。
命令通常通过 uv run python -m runtime.harness scripts/... 或 uv run python scripts/cc_math/... 调用。指南还提供了工具选择决策树，按“符号计算 / 证明或约束 / 数值计算 / 验证推理 / 学习练习 / 形式化证明”六类问题引导选择。
适用场景
- 需要精确符号解、微积分运算或代数化简；
- 需要证明定理、检查约束可满足性或做约束优化；
- 需要验证自己的推导步骤或证明链是否正确；
- 需要学习数学概念、获取分级提示或生成练习题；
- 需要机器验证的形式化证明；
- 需要数值计算、任意精度计算或函数绘图。
限制
指南中未提供关于收费、价格、平台支持范围、性能指标或效果保证的信息。所有数学脚本通过 uv sync 安装，依赖包括 sympy、z3-solver、numpy、scipy、mpmath、matplotlib、plotly。Lean 4 的完整文档需参考 /lean4 skill。