⚡

数学认知堆栈指南Skill math-help

这个技能是一个数学认知堆栈指南，提供多种数学工具和方法的详细说明，帮助用户进行符号计算、约束求解、推理验证、学习和教学。适用于数学学习者、教育工作者和需要数学计算的专业人士。关键词：数学计算、符号代数、Z3、验证、学习、工具、指南。

教育技术 0 次安装 0 次浏览 更新于 3/14/2026

name: math-help description: Guide to the math cognitive stack - what tools exist and when to use each triggers: [“help”, “guide”, “how do I”, “what math”, “math help”, “math tools”, “which tool”, “math tutorial”] user-invocable: false

数学认知堆栈指南

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

快速参考

我想要… 使用这个 示例
解方程 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 "..."
绘制2D/3D函数 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（符号代数）

何时使用： 精确代数计算 - 求解、微积分、简化、矩阵代数。

关键命令：

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

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

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

# 微分（二阶）
uv run python -m runtime.harness scripts/sympy_compute.py \
    diff "x**3" --var x --order 2

# 简化（三角函数策略）
uv run python -m runtime.harness scripts/sympy_compute.py \
    simplify "sin(x)**2 + cos(x)**2" --strategy trig

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

# 矩阵特征值
uv run python -m runtime.harness scripts/sympy_compute.py \
    eigenvalues "[[1,2],[3,4]]"

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

层次 2: Z3（约束求解和定理证明）

何时使用： 证明定理、检查可满足性、约束优化。

关键命令：

# 证明交换律
uv run python -m runtime.harness scripts/cc_math/z3_solve.py \
    prove "x + y == y + x" --vars x y --type int

# 检查可满足性
uv run python -m runtime.harness scripts/cc_math/z3_solve.py \
    sat "x > 0, x < 10, x*x == 49" --type int

# 优化
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: 数学草稿本（推理验证）

何时使用： 验证逐步推理、检查推导链。

关键命令：

# 验证单步
uv run python -m runtime.harness scripts/cc_math/math_scratchpad.py \
    verify "x = 2 implies x^2 = 4"

# 带上下文验证
uv run python -m runtime.harness scripts/cc_math/math_scratchpad.py \
    verify "x^2 = 4" --context '{"x": 2}'

# 验证推理链
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"]'

# 解释步骤
uv run python -m runtime.harness scripts/cc_math/math_scratchpad.py \
    explain "d/dx(x^3) = 3*x^2"

最适合： 检查工作、验证推导、逐步验证。

层次 4: 数学导师（教育性）

何时使用： 学习、获取提示、生成练习题。

关键命令：

# 逐步解决方案
uv run python scripts/cc_math/math_tutor.py steps "x**2 - 5*x + 6 = 0" --operation solve

# 渐进提示（级别 1-5）
uv run python scripts/cc_math/math_tutor.py hint "Solve x**2 - 4 = 0" --level 2

# 生成练习题
uv run python scripts/cc_math/math_tutor.py generate --topic algebra --difficulty 2

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

层次 5: Lean 4（形式化证明）

何时使用： 严谨的机器验证数学证明、范畴论、类型理论。

访问： 使用 /lean4 技能获取完整文档。

最适合： 出版级证明、依赖类型、范畴论。

数值工具

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

NumPy（160 个函数）

# 矩阵操作
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]]"

# 解线性系统
uv run python scripts/cc_math/numpy_compute.py solve "[[3,1],[1,2]]" "[9,8]"

SciPy（289 个函数）

# 最小化函数
uv run python scripts/cc_math/scipy_compute.py minimize "x**2 + 2*x" "5"

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

# 曲线拟合
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 到 100 位小数
uv run python scripts/cc_math/mpmath_compute.py pi --dps 100

# 任意精度平方根
uv run python -m scripts.mpmath_compute mp_sqrt "2" --dps 100

可视化

math_plot.py

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

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

# 多个函数
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 渲染
uv run python scripts/cc_math/math_plot.py latex "\\int e^{-x^2} dx" --output equation.png

教育性功能

5 级提示系统

级别 类别 您将获得
1 概念性 总体方向、主题识别
2 策略性 使用方法、技术选择
3 战术性 具体步骤、中间目标
4 计算性 中间结果、部分解决方案
5 答案 完整解决方案与解释

用法：

# 从概念提示开始
uv run python scripts/cc_math/math_tutor.py hint "integrate x*sin(x)" --level 1

# 获取更具体的指导
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. 可选地绘图可视化
# 求解
uv run python -m runtime.harness scripts/sympy_compute.py \
    solve "x**2 - 4 = 0" --var x

# 验证解决方案有效
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. 如果卡住，获取完整解决方案
# 生成问题
uv run python scripts/cc_math/math_tutor.py generate --topic calculus --difficulty 2

# 渐进获取提示
uv run python scripts/cc_math/math_tutor.py hint "..." --level 1
uv run python scripts/cc_math/math_tutor.py hint "..." --level 2

# 完整解决方案
uv run python scripts/cc_math/math_tutor.py steps "..." --operation integrate

工作流程 3: 证明和形式化

  1. 使用 z3_solve.py 检查定理（约束级证明）
  2. 如果需要严谨证明，使用 Lean 4
# 使用 Z3 快速检查
uv run python -m runtime.harness scripts/cc_math/z3_solve.py \
    prove "x*y == y*x" --vars x y --type int

# 形式化证明，使用 /lean4 技能

选择合适的工具

是 SYMBOLIC（精确答案）吗？
  └─ 是 → 使用 SymPy
      ├─ 方程 → sympy_compute.py solve
      ├─ 微积分 → sympy_compute.py integrate/diff/limit
      └─ 简化 → sympy_compute.py simplify

是 PROOF 或 CONSTRAINT 问题吗？
  └─ 是 → 使用 Z3
      ├─ 真/假定理 → z3_solve.py prove
      ├─ 查找值 → z3_solve.py sat
      └─ 优化 → z3_solve.py optimize

是 NUMERICAL（近似答案）吗？
  └─ 是 → 使用 NumPy/SciPy
      ├─ 线性代数 → numpy_compute.py
      ├─ 优化 → scipy_compute.py minimize
      └─ 高精度 → mpmath_compute.py

需要 VERIFY 推理吗？
  └─ 是 → 使用 Math Scratchpad
      ├─ 单步 → math_scratchpad.py verify
      └─ 链 → math_scratchpad.py chain

想要 LEARN/PRACTICE 吗？
  └─ 是 → 使用 Math Tutor
      ├─ 提示 → math_tutor.py hint
      └─ 练习 → math_tutor.py generate

需要 MACHINE-VERIFIED 形式化证明吗？
  └─ 是 → 使用 Lean 4（参见 /lean4 技能）

相关技能

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

要求

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

uv sync

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