Math Help

作者 parcadeid07ff4b06b62无许可证3.9K 个星标收录于 2026年10月8日更新于 2026年10月8日仓库8个月前更新

Guide to the math cognitive stack - what tools exist and when to use each

AI 生成的概览

一份数学工具栈指南,说明该用哪种计算、证明、验证、辅导或绘图工具。

功能
该技能是一份数学计算工具集的参考指南,按层次组织:符号代数、约束求解与定理证明、推理验证、辅导以及形式化证明。它列出各工具的命令和示例调用,并提供选择流程图和常见工作流。它输出的是指引和命令示例,而不是实际计算。
适用场景
当你需要判断某项数学任务该用哪个工具时使用,例如解方程、检查证明步骤、生成练习题或绘制函数图像。也适合用来查阅所述工具的示例命令。
运行要求
该指南本身只是说明,不附带脚本。它描述的工具需要 Python 环境与 uv,以及 sympy、z3-solver、numpy、scipy、mpmath、matplotlib 和 plotly;Lean 4 通过另一个独立技能引用。

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 thisExample
Solve equationssympy_compute.py solvesolve "x**2 - 4 = 0" --var x
Integrate/differentiatesympy_compute.pyintegrate "sin(x)" --var x
Compute limitssympy_compute.py limitlimit "sin(x)/x" --var x --to 0
Matrix operationssympy_compute.py / numpy_compute.pydet "[[1,2],[3,4]]"
Verify a reasoning stepmath_scratchpad.py verifyverify "x = 2 implies x^2 = 4"
Check a proof chainmath_scratchpad.py chainchain --steps '[...]'
Get progressive hintsmath_tutor.py hinthint "Solve x^2 - 4 = 0" --level 2
Generate practice problemsmath_tutor.py generategenerate --topic algebra --difficulty 2
Prove a theorem (constraints)z3_solve.py proveprove "x + y == y + x" --vars x y
Check satisfiabilityz3_solve.py satsat "x > 0, x < 10, x*x == 49"
Optimize with constraintsz3_solve.py optimizeoptimize "x + y" --constraints "..."
Plot 2D/3D functionsmath_plot.pyplot2d "sin(x)" --range -10 10
Arbitrary precisionmpmath_compute.pypi --dps 100
Numerical optimizationscipy_compute.pyminimize "x**2 + 2*x" "5"
Formal machine proofLean 4 (lean4 skill)/lean4

The Five Layers

Layer 1: SymPy (Symbolic Algebra)

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

Key Commands:

bash
# Solve equationuv run python -m runtime.harness scripts/sympy_compute.py \    solve "x**2 - 5*x + 6 = 0" --var x --domain real
# Integrateuv run python -m runtime.harness scripts/sympy_compute.py \    integrate "sin(x)" --var x
# Definite integraluv 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
# Limituv run python -m runtime.harness scripts/sympy_compute.py \    limit "sin(x)/x" --var x --to 0
# Matrix eigenvaluesuv 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:

bash
# Prove commutativityuv run python -m runtime.harness scripts/cc_math/z3_solve.py \    prove "x + y == y + x" --vars x y --type int
# Check satisfiabilityuv run python -m runtime.harness scripts/cc_math/z3_solve.py \    sat "x > 0, x < 10, x*x == 49" --type int
# Optimizeuv 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:

bash
# Verify single stepuv run python -m runtime.harness scripts/cc_math/math_scratchpad.py \    verify "x = 2 implies x^2 = 4"
# Verify with contextuv run python -m runtime.harness scripts/cc_math/math_scratchpad.py \    verify "x^2 = 4" --context '{"x": 2}'
# Verify chain of reasoninguv 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 stepuv 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:

bash
# Step-by-step solutionuv run python scripts/cc_math/math_tutor.py steps "x**2 - 5*x + 6 = 0" --operation solve
# Progressive hint (level 1-5)uv run python scripts/cc_math/math_tutor.py hint "Solve x**2 - 4 = 0" --level 2
# Generate practice problemuv 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)

bash
# Matrix operationsuv 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 systemuv run python scripts/cc_math/numpy_compute.py solve "[[3,1],[1,2]]" "[9,8]"

SciPy (289 functions)

bash
# Minimize functionuv run python scripts/cc_math/scipy_compute.py minimize "x**2 + 2*x" "5"
# Find rootuv run python scripts/cc_math/scipy_compute.py root "x**3 - x - 2" "1.5"
# Curve fittinguv 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)

bash
# Pi to 100 decimal placesuv run python scripts/cc_math/mpmath_compute.py pi --dps 100
# Arbitrary precision sqrtuv run python -m scripts.mpmath_compute mp_sqrt "2" --dps 100

Visualization

math_plot.py

bash
# 2D plotuv run python scripts/cc_math/math_plot.py plot2d "sin(x)" \    --var x --range -10 10 --output plot.png
# 3D surfaceuv run python scripts/cc_math/math_plot.py plot3d "x**2 + y**2" \    --xvar x --yvar y --range 5 --output surface.html
# Multiple functionsuv 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 renderinguv run python scripts/cc_math/math_plot.py latex "\\int e^{-x^2} dx" --output equation.png

Educational Features

5-Level Hint System

LevelCategoryWhat You Get
1ConceptualGeneral direction, topic identification
2StrategicApproach to use, technique selection
3TacticalSpecific steps, intermediate goals
4ComputationalIntermediate results, partial solutions
5AnswerFull solution with explanation

Usage:

bash
# Start with conceptual hintuv run python scripts/cc_math/math_tutor.py hint "integrate x*sin(x)" --level 1
# Get more specific guidanceuv run python scripts/cc_math/math_tutor.py hint "integrate x*sin(x)" --level 3

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

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)
bash
# Solveuv run python -m runtime.harness scripts/sympy_compute.py \    solve "x**2 - 4 = 0" --var x
# Verify the solutions workuv run python -m runtime.harness scripts/cc_math/math_scratchpad.py \    verify "x = 2 implies x^2 - 4 = 0"

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
bash
# Generate problemuv run python scripts/cc_math/math_tutor.py generate --topic calculus --difficulty 2
# Get hints progressivelyuv run python scripts/cc_math/math_tutor.py hint "..." --level 1uv run python scripts/cc_math/math_tutor.py hint "..." --level 2
# Full solutionuv run python scripts/cc_math/math_tutor.py steps "..." --operation integrate

Workflow 3: Prove and Formalize

  1. Check theorem with z3_solve.py (constraint-level proof)
  2. If rigorous proof needed, use Lean 4
bash
# Quick check with Z3uv run python -m runtime.harness scripts/cc_math/z3_solve.py \    prove "x*y == y*x" --vars x y --type int
# For formal proof, use /lean4 skill

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)

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:

bash
uv sync

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

来源与署名

来源:parcadei/continuous-claude-v3位于.claude/skills/math-help提交d07ff4b

许可证: 无许可证

内容归原作者所有。SourceWeft 从公开仓库中收录这些内容。

举报或申请下架