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: 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 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: 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 1. Solve with sympy compute.py 2. Verify solution with math scratchpad.py 3. Plot to visualize (optional) Workflow 2: Learn a Concept 1. Generate practice problem with math tutor.py 2. Use progressive hints (level 1, then 2, etc.) 3. Get full solution if stuck Workflow 3: Prove and Formalize 1. Check theorem with z3 solve.py (constraint level proof) 2. If rigorous proof needed, use Lean 4 Choosing the Right Tool Related Skills /math or /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

math-help