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 + 2*x" "5" |
| Formal machine proof |
Lean 4 (lean4 skill) |
/lean4 |
The Five Layers
Layer 1: SymPy (Symbolic Algebra)
When: Exact algebraic computation - solving, calculus, simplification, matrix algebra.
Key Commands:
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]]"
Best For: Closed-form solutions, calculus, exact algebra.
Layer 2: Z3 (Constraint Solving & Theorem Proving)
When: Proving theorems, checking satisfiability, constraint optimization.
Key Commands:
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
Best For: Logical proofs, constraint satisfaction, optimization with constraints.
Layer 3: Math Scratchpad (Reasoning Verification)
When: Verifying step-by-step reasoning, checking derivation chains.
Key Commands:
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"
Best For: Checking your work, validating derivations, step-by-step verification.
Layer 4: Math Tutor (Educational)
When: Learning, getting hints, generating practice problems.
Key Commands:
uv run python scripts/cc_math/math_tutor.py steps "x**2 - 5*x + 6 = 0" --operation solve
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
Best For: Learning, tutoring, practice.
Layer 5: Lean 4 (Formal Proofs)
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.
Numerical Tools
For numerical (not symbolic) computation:
NumPy (160 functions)
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 functions)
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 functions, arbitrary precision)
uv run python scripts/cc_math/mpmath_compute.py pi --dps 100
uv run python -m scripts.mpmath_compute mp_sqrt "2" --dps 100
Visualization
math_plot.py
uv run python scripts/cc_math/math_plot.py plot2d "sin(x)" \
--var x --range -10 10 --output plot.png
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
uv run python scripts/cc_math/math_plot.py latex "\\int e^{-x^2} dx" --output equation.png
Educational Features
5-Level Hint System
| 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:
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
Step-by-Step Solutions
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
Common Workflows
Workflow 1: Solve and Verify
- Solve with sympy_compute.py
- Verify solution with math_scratchpad.py
- Plot to visualize (optional)
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"
Workflow 2: Learn a Concept
- Generate practice problem with math_tutor.py
- Use progressive hints (level 1, then 2, etc.)
- Get full solution if stuck
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
Workflow 3: Prove and Formalize
- Check theorem with z3_solve.py (constraint-level proof)
- If rigorous proof needed, use Lean 4
uv run python -m runtime.harness scripts/cc_math/z3_solve.py \
prove "x*y == y*x" --vars x y --type int
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-VE
