Math Cognitive Stack Guide

数学认知工具栈指南

Cognitive prosthetics for exact mathematical computation. This guide helps you choose the right tool for your math task.

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

Quick Reference

快速参考

I want to...	Use this	Example
Solve equations	sympy_compute.py solve	`solve "x**2 - 4 = 0" --var x`
Integrate/differentiate	sympy_compute.py	`integrate "sin(x)" --var x`
Compute limits	sympy_compute.py limit	`limit "sin(x)/x" --var x --to 0`
Matrix operations	sympy_compute.py / numpy_compute.py	`det "[[1,2],[3,4]]"`
Verify a reasoning step	math_scratchpad.py verify	`verify "x = 2 implies x^2 = 4"`
Check a proof chain	math_scratchpad.py chain	`chain --steps '[...]'`
Get progressive hints	math_tutor.py hint	`hint "Solve x^2 - 4 = 0" --level 2`
Generate practice problems	math_tutor.py generate	`generate --topic algebra --difficulty 2`
Prove a theorem (constraints)	z3_solve.py prove	`prove "x + y == y + x" --vars x y`
Check satisfiability	z3_solve.py sat	`sat "x > 0, x < 10, x*x == 49"`
Optimize with constraints	z3_solve.py optimize	`optimize "x + y" --constraints "..."`
Plot 2D/3D functions	math_plot.py	`plot2d "sin(x)" --range -10 10`
Arbitrary precision	mpmath_compute.py	`pi --dps 100`
Numerical optimization	scipy_compute.py	`minimize "x*2 + 2x" "5"`
Formal machine proof	Lean 4 (lean4 skill)	`/lean4`

我想要...	使用这个工具	示例
解方程	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 + 2x" "5"`
形式化机器证明	Lean 4 (lean4 skill)	`/lean4`

The Five Layers

五大层级

Layer 1: SymPy (Symbolic Algebra)

层级1：SymPy（符号代数）

When: Exact algebraic computation - solving, calculus, simplification, matrix algebra.

Key Commands:

bash

undefined

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

核心命令：

bash

undefined

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]]"


**Best For:** Closed-form solutions, calculus, exact algebra.

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


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

Layer 2: Z3 (Constraint Solving & Theorem Proving)

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

When: Proving theorems, checking satisfiability, constraint optimization.

Key Commands:

bash

undefined

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

核心命令：

bash

undefined

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


**Best For:** Logical proofs, constraint satisfaction, optimization with constraints.

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


**最适合：** 逻辑证明、约束满足、带约束的优化。

Layer 3: Math Scratchpad (Reasoning Verification)

层级3：Math Scratchpad（推理验证）

When: Verifying step-by-step reasoning, checking derivation chains.

Key Commands:

bash

undefined

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

核心命令：

bash

undefined

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"


**Best For:** Checking your work, validating derivations, step-by-step verification.

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


**最适合：** 检查计算过程、验证推导、逐步验证。

Layer 4: Math Tutor (Educational)

层级4：Math Tutor（教育辅助）

When: Learning, getting hints, generating practice problems.

Key Commands:

bash

undefined

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

核心命令：

bash

undefined

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)

渐进式提示（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


**Best For:** Learning, tutoring, practice.

uv run python scripts/cc_math/math_tutor.py generate --topic algebra --difficulty 2


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

Layer 5: Lean 4 (Formal Proofs)

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

When: Rigorous machine-verified mathematical proofs, category theory, type theory.

Access: Use

/lean4

skill for full documentation.

Best For: Publication-grade proofs, dependent types, category theory.

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

使用方式： 使用

/lean4

skill获取完整文档。

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

Numerical Tools

数值计算工具

For numerical (not symbolic) computation:

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

NumPy (160 functions)

NumPy（160个函数）

bash

undefined

bash

undefined

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]"

undefined

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

undefined

SciPy (289 functions)

SciPy（289个函数）

bash

undefined

bash

undefined

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 "aexp(-bx)" "0,1,2,3" "1,0.6,0.4,0.2" "1,0.5"

undefined

uv run python scripts/cc_math/scipy_compute.py curve_fit "aexp(-bx)" "0,1,2,3" "1,0.6,0.4,0.2" "1,0.5"

undefined

mpmath (153 functions, arbitrary precision)

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

bash

undefined

bash

undefined

Pi to 100 decimal places

计算圆周率到100位小数

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

undefined

uv run python -m scripts.mpmath_compute mp_sqrt "2" --dps 100

undefined

Visualization

可视化工具

math_plot.py

bash

undefined

bash

undefined

2D plot

2D图像绘制

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

3D surface

3D曲面绘制

uv run python scripts/cc_math/math_plot.py plot3d "x2 + y2"
--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

LaTeX渲染

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

undefined

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

undefined

Educational Features

教育功能

5-Level Hint System

5级提示系统

Level	Category	What You Get
1	Conceptual	General direction, topic identification
2	Strategic	Approach to use, technique selection
3	Tactical	Specific steps, intermediate goals
4	Computational	Intermediate results, partial solutions
5	Answer	Full solution with explanation

Usage:

bash

undefined

级别	类别	内容说明
1	概念性	总体方向、主题识别
2	策略性	适用方法、技术选择
3	战术性	具体步骤、中间目标
4	计算性	中间结果、部分解答
5	答案	完整解答及说明

使用方式：

bash

undefined

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

undefined

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

undefined

Step-by-Step Solutions

分步解答

bash

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

Returns structured steps with:

Step number and type
From/to expressions
Rule applied
Justification

bash

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

返回结构化步骤，包含：

步骤编号与类型
前后表达式
应用规则
理由说明

Common Workflows

常见工作流

Workflow 1: Solve and Verify

工作流1：求解与验证

Solve with sympy_compute.py
Verify solution with math_scratchpad.py
Plot to visualize (optional)

bash

undefined

使用sympy_compute.py求解
使用math_scratchpad.py验证解
（可选）绘制图像可视化

bash

undefined

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"

undefined

uv run python -m runtime.harness scripts/cc_math/math_scratchpad.py
verify "x = 2 implies x^2 - 4 = 0"

undefined

Workflow 2: Learn a Concept

工作流2：学习概念

Generate practice problem with math_tutor.py
Use progressive hints (level 1, then 2, etc.)
Get full solution if stuck

bash

undefined

使用math_tutor.py生成练习题
使用渐进式提示（先1级，再2级等）
若遇到困难，获取完整解答

bash

undefined

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

undefined

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

undefined

Workflow 3: Prove and Formalize

工作流3：证明与形式化

Check theorem with z3_solve.py (constraint-level proof)
If rigorous proof needed, use Lean 4

bash

undefined

使用z3_solve.py检查定理（约束级证明）
若需要严谨证明，使用Lean 4

bash

undefined

Quick check with Z3

使用Z3快速检查

uv run python -m runtime.harness scripts/cc_math/z3_solve.py
prove "xy == yx" --vars x y --type int

For formal proof, use /lean4 skill

如需形式化证明，使用/lean4 skill

undefined

undefined

Choosing the Right Tool

工具选择指南

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)

是否需要符号计算（精确答案）？
  └─ 是 → 使用SymPy
      ├─ 解方程 → sympy_compute.py solve
      ├─ 微积分 → sympy_compute.py integrate/diff/limit
      └─ 化简 → sympy_compute.py simplify

是否是证明或约束类问题？
  └─ 是 → 使用Z3
      ├─ 真假性定理证明 → z3_solve.py prove
      ├─ 寻找可行值 → z3_solve.py sat
      └─ 优化问题 → z3_solve.py optimize

是否需要数值计算（近似答案）？
  └─ 是 → 使用NumPy/SciPy
      ├─ 线性代数 → numpy_compute.py
      ├─ 优化问题 → scipy_compute.py minimize
      └─ 高精度计算 → mpmath_compute.py

是否需要验证推理过程？
  └─ 是 → 使用Math Scratchpad
      ├─ 单步验证 → math_scratchpad.py verify
      └─ 推理链验证 → math_scratchpad.py chain

是否需要学习/练习？
  └─ 是 → 使用Math Tutor
      ├─ 获取提示 → math_tutor.py hint
      └─ 生成练习题 → math_tutor.py generate

是否需要机器验证的形式化证明？
  └─ 是 → 使用Lean 4（查看/lean4 skill）

Related Skills

Requirements

环境要求

All math scripts are installed via:

bash

uv sync

Dependencies: sympy, z3-solver, numpy, scipy, mpmath, matplotlib, plotly

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

bash

uv sync

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

math-help

Original

Translation

Math Cognitive Stack Guide

数学认知工具栈指南

Quick Reference

快速参考

The Five Layers

五大层级

Layer 1: SymPy (Symbolic Algebra)

层级1：SymPy（符号代数）

Solve equation

解方程

Integrate

积分

Definite integral

定积分

Differentiate (2nd order)

求导（二阶）

Simplify (trig strategy)

化简（三角策略）

Limit

计算极限

Matrix eigenvalues

矩阵特征值

Layer 2: Z3 (Constraint Solving & Theorem Proving)

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

Prove commutativity

证明交换律

Check satisfiability

检查可满足性

Optimize

优化

Layer 3: Math Scratchpad (Reasoning Verification)

层级3：Math Scratchpad（推理验证）

Verify single step

验证单步推理

Verify with context

带上下文验证

Verify chain of reasoning

验证推理链

Explain a step

解释步骤

Layer 4: Math Tutor (Educational)

层级4：Math Tutor（教育辅助）

Step-by-step solution

分步解答

Progressive hint (level 1-5)

渐进式提示（1-5级）

Generate practice problem

生成练习题

Layer 5: Lean 4 (Formal Proofs)

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

Numerical Tools

数值计算工具

NumPy (160 functions)

NumPy（160个函数）

Matrix operations

矩阵运算

Solve linear system

解线性方程组

SciPy (289 functions)

SciPy（289个函数）

Minimize function

函数最小化

Find root

找根

Curve fitting

曲线拟合

mpmath (153 functions, arbitrary precision)

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

Pi to 100 decimal places

计算圆周率到100位小数

Arbitrary precision sqrt

任意精度平方根

Visualization

可视化工具

math_plot.py

math_plot.py

2D plot