{"id":"math-help","name":"math-help","summary":"数学認知スタックガイド - 存在するツールとそれぞれの使い方のタイミング","body":"# Math Cognitive Stack Guide\n\nCognitive prosthetics for exact mathematical computation. This guide helps you choose the right tool for your math task.\n\n## Quick Reference\n\n| I want to... | Use this | Example |\n|--------------|----------|---------|\n| Solve equations | sympy_compute.py solve | `solve \"x**2 - 4 = 0\" --var x` |\n| Integrate/differentiate | sympy_compute.py | `integrate \"sin(x)\" --var x` |\n| Compute limits | sympy_compute.py limit | `limit \"sin(x)/x\" --var x --to 0` |\n| Matrix operations | sympy_compute.py / numpy_compute.py | `det \"[[1,2],[3,4]]\"` |\n| Verify a reasoning step | math_scratchpad.py verify | `verify \"x = 2 implies x^2 = 4\"` |\n| Check a proof chain | math_scratchpad.py chain | `chain --steps '[...]'` |\n| Get progressive hints | math_tutor.py hint | `hint \"Solve x^2 - 4 = 0\" --level 2` |\n| Generate practice problems | math_tutor.py generate | `generate --topic algebra --difficulty 2` |\n| Prove a theorem (constraints) | z3_solve.py prove | `prove \"x + y == y + x\" --vars x y` |\n| Check satisfiability | z3_solve.py sat | `sat \"x > 0, x < 10, x*x == 49\"` |\n| Optimize with constraints | z3_solve.py optimize | `optimize \"x + y\" --constraints \"...\"` |\n| Plot 2D/3D functions | math_plot.py | `plot2d \"sin(x)\" --range -10 10` |\n| Arbitrary precision | mpmath_compute.py | `pi --dps 100` |\n| Numerical optimization | scipy_compute.py | `minimize \"x**2 + 2*x\" \"5\"` |\n| Formal machine proof | Lean 4 (lean4 skill) | `/lean4` |\n\n## The Five Layers\n\n### Layer 1: SymPy (Symbolic Algebra)\n\n**When:** Exact algebraic computation - solving, calculus, simplification, matrix algebra.\n\n**Key Commands:**\n```bash\n# Solve equation\nuv run python -m runtime.harness scripts/sympy_compute.py \\\n    solve \"x**2 - 5*x + 6 = 0\" --var x --domain real\n\n# Integrate\nuv run python -m runtime.harness scripts/sympy_compute.py \\\n    integrate \"sin(x)\" --var x\n\n# Definite integral\nuv run python -m runtime.harness scripts/sympy_compute.py \\\n    integrate \"x**2\" --var x --bounds 0 1\n\n# Differentiate (2nd order)\nuv run python -m runtime.harness scripts/sympy_compute.py \\\n    diff \"x**3\" --var x --order 2\n\n# Simplify (trig strategy)\nuv run python -m runtime.harness scripts/sympy_compute.py \\\n    simplify \"sin(x)**2 + cos(x)**2\" --strategy trig\n\n# Limit\nuv run python -m runtime.harness scripts/sympy_compute.py \\\n    limit \"sin(x)/x\" --var x --to 0\n\n# Matrix eigenvalues\nuv run python -m runtime.harness scripts/sympy_compute.py \\\n    eigenvalues \"[[1,2],[3,4]]\"\n```\n\n**Best For:** Closed-form solutions, calculus, exact algebra.\n\n### Layer 2: Z3 (Constraint Solving & Theorem Proving)\n\n**When:** Proving theorems, checking satisfiability, constraint optimization.\n\n**Key Commands:**\n```bash\n# Prove commutativity\nuv run python -m runtime.harness scripts/cc_math/z3_solve.py \\\n    prove \"x + y == y + x\" --vars x y --type int\n\n# Check satisfiability\nuv run python -m runtime.harness scripts/cc_math/z3_solve.py \\\n    sat \"x > 0, x < 10, x*x == 49\" --type int\n\n# Optimize\nuv run python -m runtime.harness scripts/cc_math/z3_solve.py \\\n    optimize \"x + y\" --constraints \"x >= 0, y >= 0, x + y <= 100\" \\\n    --direction maximize --type real\n```\n\n**Best For:** Logical proofs, constraint satisfaction, optimization with constraints.\n\n### Layer 3: Math Scratchpad (Reasoning Verification)\n\n**When:** Verifying step-by-step reasoning, checking derivation chains.\n\n**Key Commands:**\n```bash\n# Verify single step\nuv run python -m runtime.harness scripts/cc_math/math_scratchpad.py \\\n    verify \"x = 2 implies x^2 = 4\"\n\n# Verify with context\nuv run python -m runtime.harness scripts/cc_math/math_scratchpad.py \\\n    verify \"x^2 = 4\" --context '{\"x\": 2}'\n\n# Verify chain of reasoning\nuv run python -m runtime.harness scripts/cc_math/math_scratchpad.py \\\n    chain --steps '[\"x^2 - 4 = 0\", \"(x-2)(x+2) = 0\", \"x = 2 or x = -2\"]'\n\n# Explain a step\nuv run python -m runtime.harness scripts/cc_math/math_scratchpad.py \\\n    explain \"d/dx(x^3) = 3*x^2\"\n```\n\n**Best For:** Checking your work, validating derivations, step-by-step verification.\n\n### Layer 4: Math Tutor (Educational)\n\n**When:** Learning, getting hints, generating practice problems.\n\n**Key Commands:**\n```bash\n# Step-by-step solution\nuv run python scripts/cc_math/math_tutor.py steps \"x**2 - 5*x + 6 = 0\" --operation solve\n\n# Progressive hint (level 1-5)\nuv run python scripts/cc_math/math_tutor.py hint \"Solve x**2 - 4 = 0\" --level 2\n\n# Generate practice problem\nuv run python scripts/cc_math/math_tutor.py generate --topic algebra --difficulty 2\n```\n\n**Best For:** Learning, tutoring, practice.\n\n### Layer 5: Lean 4 (Formal Proofs)\n\n**When:** Rigorous machine-verified mathematical proofs, category theory, type theory.\n\n**Access:** Use `/lean4` skill for full documentation.\n\n**Best For:** Publication-grade proofs, dependent types, category theory.\n\n## Numerical Tools\n\nFor numerical (not symbolic) computation:\n\n### NumPy (160 functions)\n```bash\n# Matrix operations\nuv run python scripts/cc_math/numpy_compute.py det \"[[1,2],[3,4]]\"\nuv run python scripts/cc_math/numpy_compute.py inv \"[[1,2],[3,4]]\"\nuv run python scripts/cc_math/numpy_compute.py eig \"[[1,2],[3,4]]\"\nuv run python scripts/cc_math/numpy_compute.py svd \"[[1,2,3],[4,5,6]]\"\n\n# Solve linear system\nuv run python scripts/cc_math/numpy_compute.py solve \"[[3,1],[1,2]]\" \"[9,8]\"\n```\n\n### SciPy (289 functions)\n```bash\n# Minimize function\nuv run python scripts/cc_math/scipy_compute.py minimize \"x**2 + 2*x\" \"5\"\n\n# Find root\nuv run python scripts/cc_math/scipy_compute.py root \"x**3 - x - 2\" \"1.5\"\n\n# Curve fitting\nuv 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\"\n```\n\n### mpmath (153 functions, arbitrary precision)\n```bash\n# Pi to 100 decimal places\nuv run python scripts/cc_math/mpmath_compute.py pi --dps 100\n\n# Arbitrary precision sqrt\nuv run python -m scripts.mpmath_compute mp_sqrt \"2\" --dps 100\n```\n\n## Visualization\n\n### math_plot.py\n```bash\n# 2D plot\nuv run python scripts/cc_math/math_plot.py plot2d \"sin(x)\" \\\n    --var x --range -10 10 --output plot.png\n\n# 3D surface\nuv run python scripts/cc_math/math_plot.py plot3d \"x**2 + y**2\" \\\n    --xvar x --yvar y --range 5 --output surface.html\n\n# Multiple functions\nuv run python scripts/cc_math/math_plot.py plot2d-multi \"sin(x),cos(x)\" \\\n    --var x --range -6.28 6.28 --output multi.png\n\n# LaTeX rendering\nuv run python scripts/cc_math/math_plot.py latex \"\\\\int e^{-x^2} dx\" --output equation.png\n```\n\n## Educational Features\n\n### 5-Level Hint System\n\n| Level | Category | What You Get |\n|-------|----------|--------------|\n| 1 | Conceptual | General direction, topic identification |\n| 2 | Strategic | Approach to use, technique selection |\n| 3 | Tactical | Specific steps, intermediate goals |\n| 4 | Computational | Intermediate results, partial solutions |\n| 5 | Answer | Full solution with explanation |\n\n**Usage:**\n```bash\n# Start with conceptual hint\nuv run python scripts/cc_math/math_tutor.py hint \"integrate x*sin(x)\" --level 1\n\n# Get more specific guidance\nuv run python scripts/cc_math/math_tutor.py hint \"integrate x*sin(x)\" --level 3\n```\n\n### Step-by-Step Solutions\n\n```bash\nuv run python scripts/cc_math/math_tutor.py steps \"x**2 - 5*x + 6 = 0\" --operation solve\n```\n\nReturns structured steps with:\n- Step number and type\n- From/to expressions\n- Rule applied\n- Justification\n\n## Common Workflows\n\n### Workflow 1: Solve and Verify\n1. Solve with sympy_compute.py\n2. Verify solution with math_scratchpad.py\n3. Plot to visualize (optional)\n\n```bash\n# Solve\nuv run python -m runtime.harness scripts/sympy_compute.py \\\n    solve \"x**2 - 4 = 0\" --var x\n\n# Verify the solutions work\nuv run python -m runtime.harness scripts/cc_math/math_scratchpad.py \\\n    verify \"x = 2 implies x^2 - 4 = 0\"\n```\n\n### Workflow 2: Learn a Concept\n1. Generate practice problem with math_tutor.py\n2. Use progressive hints (level 1, then 2, etc.)\n3. Get full solution if stuck\n\n```bash\n# Generate problem\nuv run python scripts/cc_math/math_tutor.py generate --topic calculus --difficulty 2\n\n# Get hints progressively\nuv run python scripts/cc_math/math_tutor.py hint \"...\" --level 1\nuv run python scripts/cc_math/math_tutor.py hint \"...\" --level 2\n\n# Full solution\nuv run python scripts/cc_math/math_tutor.py steps \"...\" --operation integrate\n```\n\n### Workflow 3: Prove and Formalize\n1. Check theorem with z3_solve.py (constraint-level proof)\n2. If rigorous proof needed, use Lean 4\n\n```bash\n# Quick check with Z3\nuv run python -m runtime.harness scripts/cc_math/z3_solve.py \\\n    prove \"x*y == y*x\" --vars x y --type int\n\n# For formal proof, use /lean4 skill\n```\n\n## Choosing the Right Tool\n\n```\nIs it SYMBOLIC (exact answers)?\n  └─ Yes → Use SymPy\n      ├─ Equations → sympy_compute.py solve\n      ├─ Calculus → sympy_compute.py integrate/diff/limit\n      └─ Simplify → sympy_compute.py simplify\n\nIs it a PROOF or CONSTRAINT problem?\n  └─ Yes → Use Z3\n      ├─ True/False theorem → z3_solve.py prove\n      ├─ Find values → z3_solve.py sat\n      └─ Optimize → z3_solve.py optimize\n\nIs it NUMERICAL (approximate answers)?\n  └─ Yes → Use NumPy/SciPy\n      ├─ Linear algebra → numpy_compute.py\n      ├─ Optimization → scipy_compute.py minimize\n      └─ High precision → mpmath_compute.py\n\nNeed to VERIFY reasoning?\n  └─ Yes → Use Math Scratchpad\n      ├─ Single step → math_scratchpad.py verify\n      └─ Chain → math_scratchpad.py chain\n\nWant to LEARN/PRACTICE?\n  └─ Yes → Use Math Tutor\n      ├─ Hints → math_tutor.py hint\n      └─ Practice → math_tutor.py generate\n\nNeed MACHINE-VERIFIED formal proof?\n  └─ Yes → Use Lean 4 (see /lean4 skill)\n```\n\n## Related Skills\n\n- `/math` or `/math-mode` - Quick access to the orchestration skill\n- `/lean4` - Formal theorem proving with Lean 4\n- `/lean4-functors` - Category theory functors\n- `/lean4-nat-trans` - Natural transformations\n- `/lean4-limits` - Limits and colimits\n\n## Requirements\n\nAll math scripts are installed via:\n```bash\nuv sync\n```\n\nDependencies: sympy, z3-solver, numpy, scipy, mpmath, matplotlib, plotly","author":"@parcadei","ownerProfile":null,"authorContacts":null,"sourceUrl":"https://github.com/parcadei/Continuous-Claude-v3/tree/main/.claude/skills/math-help","license":"MIT","category":"productivity","lang":"en","tokens":2937,"stars":0,"calls30d":1,"claimed":false,"visibility":"public","origin":"crawler","version":"0.1.0","createdAt":"2026-08-22","updatedAt":"2026-08-22","files":[],"requires":{"mcp":[],"tools":[]},"safety":{"flags":[],"scannedAt":"2026-08-22","hasScripts":false,"networkEndpoints":[]}}