math-help

数学认知工具栈指南

用于精确数学计算的认知辅助工具。本指南可帮助你为数学任务选择合适的工具。

快速参考

我想要……	使用此工具	示例
求解方程	sympy_compute.py solve	solve "x**2 - 4 = 0" --var x
积分/求导	sympy_compute.py	integrate "sin(x)" --var x
计算极限	sympy_compute.py limit	limit "sin(x)/x" --var x --to 0
矩阵运算	sympy_compute.py / numpy_compute.py	det "[[1,2],[3,4]]"
验证推理步骤	math_scratchpad.py verify	verify "x = 2 implies x^2 = 4"
检查证明链	math_scratchpad.py chain	chain --steps '[...]'
获取渐进式提示	math_tutor.py hint	hint "Solve x^2 - 4 = 0" --level 2
生成练习题	math_tutor.py generate	generate --topic algebra --difficulty 2
证明定理（约束条件）	z3_solve.py prove	prove "x + y == y + x" --vars x y
检查可满足性	z3_solve.py sat	sat "x > 0, x < 10, x*x == 49"
在约束条件下优化	z3_solve.py optimize	optimize "x + y" --constraints "..."
绘制二维/三维函数	math_plot.py	plot2d "sin(x)" --range -10 10
任意精度计算	mpmath_compute.py	pi --dps 100
数值优化	scipy_compute.py	minimize "x**2 + 2*x" "5"
形式化机器证明	Lean 4（lean4 skill）	/lean4

五个层级

第 1 层：SymPy（符号代数）

适用场景： 精确代数计算——求解、微积分、化简、矩阵代数。

主要命令：

# Solve equation
uv run python -m runtime.harness scripts/sympy_compute.py \
    solve "x**2 - 5*x + 6 = 0" --var x --domain real

# Integrate
uv run python -m runtime.harness scripts/sympy_compute.py \
    integrate "sin(x)" --var x

# Definite integral
uv run python -m runtime.harness scripts/sympy_compute.py \
    integrate "x**2" --var x --bounds 0 1

# Differentiate (2nd order)
uv run python -m runtime.harness scripts/sympy_compute.py \
    diff "x**3" --var x --order 2

# Simplify (trig strategy)
uv run python -m runtime.harness scripts/sympy_compute.py \
    simplify "sin(x)**2 + cos(x)**2" --strategy trig

# Limit
uv run python -m runtime.harness scripts/sympy_compute.py \
    limit "sin(x)/x" --var x --to 0

# Matrix eigenvalues
uv run python -m runtime.harness scripts/sympy_compute.py \
    eigenvalues "[[1,2],[3,4]]"

最适合： 闭式解、微积分、精确代数。

第 2 层：Z3（约束求解与定理证明）

适用场景： 证明定理、检查可满足性、约束优化。

主要命令：

# Prove commutativity
uv run python -m runtime.harness scripts/cc_math/z3_solve.py \
    prove "x + y == y + x" --vars x y --type int

# Check satisfiability
uv run python -m runtime.harness scripts/cc_math/z3_solve.py \
    sat "x > 0, x < 10, x*x == 49" --type int

# Optimize
uv run python -m runtime.harness scripts/cc_math/z3_solve.py \
    optimize "x + y" --constraints "x >= 0, y >= 0, x + y <= 100" \
    --direction maximize --type real

最适合： 逻辑证明、约束满足、约束条件下的优化。

第 3 层：数学草稿板（推理验证）

适用场景： 验证逐步推理、检查推导链。

主要命令：

# Verify single step
uv run python -m runtime.harness scripts/cc_math/math_scratchpad.py \
    verify "x = 2 implies x^2 = 4"

# Verify with context
uv run python -m runtime.harness scripts/cc_math/math_scratchpad.py \
    verify "x^2 = 4" --context '{"x": 2}'

# Verify chain of reasoning
uv run python -m runtime.harness scripts/cc_math/math_scratchpad.py \
    chain --steps '["x^2 - 4 = 0", "(x-2)(x+2) = 0", "x = 2 or x = -2"]'

# Explain a step
uv run python -m runtime.harness scripts/cc_math/math_scratchpad.py \
    explain "d/dx(x^3) = 3*x^2"

最适合： 检查解答、验证推导、逐步验证。

第 4 层：数学导师（教育）

适用场景： 学习、获取提示、生成练习题。

主要命令：

# Step-by-step solution
uv run python scripts/cc_math/math_tutor.py steps "x**2 - 5*x + 6 = 0" --operation solve

# Progressive hint (level 1-5)
uv run python scripts/cc_math/math_tutor.py hint "Solve x**2 - 4 = 0" --level 2

# Generate practice problem
uv run python scripts/cc_math/math_tutor.py generate --topic algebra --difficulty 2

最适合： 学习、辅导、练习。

第 5 层：Lean 4（形式化证明）

适用场景： 严谨且经过机器验证的数学证明、范畴论、类型论。

访问方式： 使用 /lean4 skill 查看完整文档。

最适合： 可用于发表的证明、依赖类型、范畴论。

数值工具

用于数值（而非符号）计算：

NumPy（160 个函数）

# Matrix operations
uv run python scripts/cc_math/numpy_compute.py det "[[1,2],[3,4]]"
uv run python scripts/cc_math/numpy_compute.py inv "[[1,2],[3,4]]"
uv run python scripts/cc_math/numpy_compute.py eig "[[1,2],[3,4]]"
uv run python scripts/cc_math/numpy_compute.py svd "[[1,2,3],[4,5,6]]"

# Solve linear system
uv run python scripts/cc_math/numpy_compute.py solve "[[3,1],[1,2]]" "[9,8]"

SciPy（289 个函数）

# Minimize function
uv run python scripts/cc_math/scipy_compute.py minimize "x**2 + 2*x" "5"

# Find root
uv run python scripts/cc_math/scipy_compute.py root "x**3 - x - 2" "1.5"

# Curve fitting
uv run python scripts/cc_math/scipy_compute.py curve_fit "a*exp(-b*x)" "0,1,2,3" "1,0.6,0.4,0.2" "1,0.5"

mpmath（153 个函数，支持任意精度）

# Pi to 100 decimal places
uv run python scripts/cc_math/mpmath_compute.py pi --dps 100

# Arbitrary precision sqrt
uv run python -m scripts.mpmath_compute mp_sqrt "2" --dps 100

可视化

math_plot.py

# 2D plot
uv run python scripts/cc_math/math_plot.py plot2d "sin(x)" \
    --var x --range -10 10 --output plot.png

# 3D surface
uv run python scripts/cc_math/math_plot.py plot3d "x**2 + y**2" \
    --xvar x --yvar y --range 5 --output surface.html

# Multiple functions
uv run python scripts/cc_math/math_plot.py plot2d-multi "sin(x),cos(x)" \
    --var x --range -6.28 6.28 --output multi.png

# LaTeX rendering
uv run python scripts/cc_math/math_plot.py latex "\\int e^{-x^2} dx" --output equation.png

教育功能

五级提示系统

级别	类别	可获取内容
1	概念性	大致方向、主题识别
2	策略性	使用的方法、技术选择
3	战术性	具体步骤、中间目标
4	计算性	中间结果、部分解答
5	答案	附带解释的完整解答

用法：

# Start with conceptual hint
uv run python scripts/cc_math/math_tutor.py hint "integrate x*sin(x)" --level 1

# Get more specific guidance
uv run python scripts/cc_math/math_tutor.py hint "integrate x*sin(x)" --level 3

分步解答

uv run python scripts/cc_math/math_tutor.py steps "x**2 - 5*x + 6 = 0" --operation solve

返回包含以下内容的结构化步骤：

• 步骤编号和类型
• 起始/目标表达式
• 应用的规则
• 依据

常见工作流

工作流 1：求解并验证

1. 使用 sympy_compute.py 求解
2. 使用 math_scratchpad.py 验证解答
3. 绘图以便直观查看（可选）

# Solve
uv run python -m runtime.harness scripts/sympy_compute.py \
    solve "x**2 - 4 = 0" --var x

# Verify the solutions work
uv run python -m runtime.harness scripts/cc_math/math_scratchpad.py \
    verify "x = 2 implies x^2 - 4 = 0"

工作流 2：学习概念

1. 使用 math_tutor.py 生成练习题
2. 使用渐进式提示（先级别 1，再级别 2，依此类推）
3. 如果遇到困难，获取完整解答

# Generate problem
uv run python scripts/cc_math/math_tutor.py generate --topic calculus --difficulty 2

# Get hints progressively
uv run python scripts/cc_math/math_tutor.py hint "..." --level 1
uv run python scripts/cc_math/math_tutor.py hint "..." --level 2

# Full solution
uv run python scripts/cc_math/math_tutor.py steps "..." --operation integrate

工作流 3：证明并形式化

1. 使用 z3_solve.py 检查定理（约束级证明）
2. 如果需要严格证明，则使用 Lean 4

# Quick check with Z3
uv run python -m runtime.harness scripts/cc_math/z3_solve.py \
    prove "x*y == y*x" --vars x y --type int

# For formal proof, use /lean4 skill

选择合适的工具

Is it SYMBOLIC (exact answers)?
  └─ Yes → Use SymPy
      ├─ Equations → sympy_compute.py solve
      ├─ Calculus → sympy_compute.py integrate/diff/limit
      └─ Simplify → sympy_compute.py simplify

Is it a PROOF or CONSTRAINT problem?
  └─ Yes → Use Z3
      ├─ True/False theorem → z3_solve.py prove
      ├─ Find values → z3_solve.py sat
      └─ Optimize → z3_solve.py optimize

Is it NUMERICAL (approximate answers)?
  └─ Yes → Use NumPy/SciPy
      ├─ Linear algebra → numpy_compute.py
      ├─ Optimization → scipy_compute.py minimize
      └─ High precision → mpmath_compute.py

Need to VERIFY reasoning?
  └─ Yes → Use Math Scratchpad
      ├─ Single step → math_scratchpad.py verify
      └─ Chain → math_scratchpad.py chain

Want to LEARN/PRACTICE?
  └─ Yes → Use Math Tutor
      ├─ Hints → math_tutor.py hint
      └─ Practice → math_tutor.py generate

Need MACHINE-VERIFIED formal proof?
  └─ Yes → Use Lean 4 (see /lean4 skill)

相关技能

• /math 或 /math-mode - 快速访问编排技能
• /lean4 - 使用 Lean 4 进行形式化定理证明
• /lean4-functors - 范畴论函子
• /lean4-nat-trans - 自然变换
• /lean4-limits - 极限与余极限

要求

所有数学脚本均通过以下方式安装：

uv sync

依赖项：sympy、z3-solver、numpy、scipy、mpmath、matplotlib、plotly