Math Cognitive Stack Guide
Cognitive prosthetics for exact mathematical computation. This guide helps you choose the right tool for your math task.
Quick Reference
The Five Layers
Layer 1: SymPy (Symbolic Algebra)
When: Exact algebraic computation - solving, calculus, simplification, matrix algebra.
Key Commands:
Best For: Closed-form solutions, calculus, exact algebra.
Layer 2: Z3 (Constraint Solving & Theorem Proving)
When: Proving theorems, checking satisfiability, constraint optimization.
Key Commands:
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:
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:
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)
SciPy (289 functions)
mpmath (153 functions, arbitrary precision)
Visualization
math_plot.py
Educational Features
5-Level Hint System
Usage:
Step-by-Step Solutions
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)
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
Workflow 3: Prove and Formalize
- Check theorem with z3_solve.py (constraint-level proof)
- If rigorous proof needed, use Lean 4
Choosing the Right Tool
Related Skills
/mathor/math-mode- Quick access to the orchestration skill/lean4- Formal theorem proving with Lean 4/lean4-functors- Category theory functors/lean4-nat-trans- Natural transformations/lean4-limits- Limits and colimits
Requirements
All math scripts are installed via:
Dependencies: sympy, z3-solver, numpy, scipy, mpmath, matplotlib, plotly



