math-help

数学認知スタックガイド

厳密な数学計算のための認知補助ツールです。このガイドでは、数学のタスクに適したツールの選び方を説明します。

クイックリファレンス

したいこと	使用するツール	例
方程式を解く	sympy_compute.py solve	solve "x**2 - 4 = 0" --var x
積分／微分する	sympy_compute.py	integrate "sin(x)" --var x
極限を計算する	sympy_compute.py limit	limit "sin(x)/x" --var x --to 0
行列演算を行う	sympy_compute.py / numpy_compute.py	det "[[1,2],[3,4]]"
推論のステップを検証する	math_scratchpad.py verify	verify "x = 2 implies x^2 = 4"
証明の連鎖を確認する	math_scratchpad.py chain	chain --steps '[...]'
段階的なヒントを得る	math_tutor.py hint	hint "Solve x^2 - 4 = 0" --level 2
練習問題を生成する	math_tutor.py generate	generate --topic algebra --difficulty 2
定理を証明する（制約）	z3_solve.py prove	prove "x + y == y + x" --vars x y
充足可能性を確認する	z3_solve.py sat	sat "x > 0, x < 10, x*x == 49"
制約付きで最適化する	z3_solve.py optimize	optimize "x + y" --constraints "..."
2D／3D関数をプロットする	math_plot.py	plot2d "sin(x)" --range -10 10
任意精度で計算する	mpmath_compute.py	pi --dps 100
数値最適化を行う	scipy_compute.py	minimize "x**2 + 2*x" "5"
機械検証による形式証明	Lean 4（lean4 skill）	/lean4

5つのレイヤー

レイヤー 1：SymPy（記号代数）

用途： 厳密な代数計算（方程式の解法、微積分、簡約、行列代数）。

主なコマンド：

# Solve equation
uv run python -m runtime.harness scripts/sympy_compute.py \
    solve "x**2 - 5*x + 6 = 0" --var x --domain real

# Integrate
uv run python -m runtime.harness scripts/sympy_compute.py \
    integrate "sin(x)" --var x

# Definite integral
uv 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

# Limit
uv run python -m runtime.harness scripts/sympy_compute.py \
    limit "sin(x)/x" --var x --to 0

# Matrix eigenvalues
uv run python -m runtime.harness scripts/sympy_compute.py \
    eigenvalues "[[1,2],[3,4]]"

最適な用途： 閉形式解、微積分、厳密な代数計算。

レイヤー 2：Z3（制約求解と定理証明）

用途： 定理の証明、充足可能性の確認、制約付き最適化。

主なコマンド：

# Prove commutativity
uv run python -m runtime.harness scripts/cc_math/z3_solve.py \
    prove "x + y == y + x" --vars x y --type int

# Check satisfiability
uv run python -m runtime.harness scripts/cc_math/z3_solve.py \
    sat "x > 0, x < 10, x*x == 49" --type int

# Optimize
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

最適な用途： 論理的な証明、制約充足、制約付き最適化。

レイヤー 3：Math Scratchpad（推論の検証）

用途： 段階的な推論の検証、導出の連鎖の確認。

主なコマンド：

# Verify single step
uv run python -m runtime.harness scripts/cc_math/math_scratchpad.py \
    verify "x = 2 implies x^2 = 4"

# Verify with context
uv run python -m runtime.harness scripts/cc_math/math_scratchpad.py \
    verify "x^2 = 4" --context '{"x": 2}'

# Verify chain of reasoning
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"]'

# Explain a step
uv run python -m runtime.harness scripts/cc_math/math_scratchpad.py \
    explain "d/dx(x^3) = 3*x^2"

最適な用途： 解答の確認、導出の検証、段階的な検証。

レイヤー 4：Math Tutor（教育）

用途： 学習、ヒントの取得、練習問題の生成。

主なコマンド：

# Step-by-step solution
uv 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 problem
uv run python scripts/cc_math/math_tutor.py generate --topic algebra --difficulty 2

最適な用途： 学習、個別指導、練習。

レイヤー 5：Lean 4（形式証明）

用途： 厳密な機械検証付き数学的証明、圏論、型理論。

アクセス： 詳細なドキュメントについては、/lean4 skill を使用してください。

最適な用途： 論文掲載レベルの証明、依存型、圏論。

数値計算ツール

数値計算（記号計算ではない）には、次のツールを使用します。

NumPy（160 関数）

# Matrix operations
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]]"

# Solve linear system
uv run python scripts/cc_math/numpy_compute.py solve "[[3,1],[1,2]]" "[9,8]"

SciPy（289 関数）

# Minimize function
uv run python scripts/cc_math/scipy_compute.py minimize "x**2 + 2*x" "5"

# Find root
uv run python scripts/cc_math/scipy_compute.py root "x**3 - x - 2" "1.5"

# Curve fitting
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 関数、任意精度）

# Pi to 100 decimal places
uv run python scripts/cc_math/mpmath_compute.py pi --dps 100

# Arbitrary precision sqrt
uv run python -m scripts.mpmath_compute mp_sqrt "2" --dps 100

可視化

math_plot.py

# 2D plot
uv run python scripts/cc_math/math_plot.py plot2d "sin(x)" \
    --var x --range -10 10 --output plot.png

# 3D surface
uv run python scripts/cc_math/math_plot.py plot3d "x**2 + y**2" \
    --xvar x --yvar y --range 5 --output surface.html

# Multiple functions
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

# LaTeX rendering
uv run python scripts/cc_math/math_plot.py latex "\\int e^{-x^2} dx" --output equation.png

学習機能

5段階のヒントシステム

レベル	カテゴリ	得られる内容
1	概念的	大まかな方向性、トピックの特定
2	戦略的	使用するアプローチ、手法の選択
3	戦術的	具体的な手順、中間目標
4	計算的	中間結果、部分的な解答
5	解答	解説付きの完全な解答

使い方：

# Start with conceptual hint
uv run python scripts/cc_math/math_tutor.py hint "integrate x*sin(x)" --level 1

# Get more specific guidance
uv run python scripts/cc_math/math_tutor.py hint "integrate x*sin(x)" --level 3

段階的な解答

uv run python scripts/cc_math/math_tutor.py steps "x**2 - 5*x + 6 = 0" --operation solve

次の項目を含む、構造化された手順を返します。

• ステップ番号と種類
• 変換前／変換後の式
• 適用した規則
• 根拠

よくあるワークフロー

ワークフロー 1：解いて検証する

1. sympy_compute.py で解く
2. math_scratchpad.py で解答を検証する
3. 可視化のためにプロットする（任意）

# Solve
uv run python -m runtime.harness scripts/sympy_compute.py \
    solve "x**2 - 4 = 0" --var x

# Verify the solutions work
uv run python -m runtime.harness scripts/cc_math/math_scratchpad.py \
    verify "x = 2 implies x^2 - 4 = 0"

ワークフロー 2：概念を学ぶ

1. math_tutor.py で練習問題を生成する
2. 段階的なヒントを使う（レベル 1、次に 2 など）
3. 行き詰まったら完全な解答を得る

# Generate problem
uv run python scripts/cc_math/math_tutor.py generate --topic calculus --difficulty 2

# Get hints progressively
uv run python scripts/cc_math/math_tutor.py hint "..." --level 1
uv run python scripts/cc_math/math_tutor.py hint "..." --level 2

# Full solution
uv run python scripts/cc_math/math_tutor.py steps "..." --operation integrate

ワークフロー 3：証明して形式化する

1. z3_solve.py で定理を確認する（制約レベルの証明）
2. 厳密な証明が必要な場合は、Lean 4 を使用する

# Quick check with Z3
uv 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

適切なツールの選び方

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)

関連スキル

• /math または /math-mode - オーケストレーションスキルにすばやくアクセスできます
• /lean4 - Lean 4 による形式的な定理証明
• /lean4-functors - 圏論の関手
• /lean4-nat-trans - 自然変換
• /lean4-limits - 極限と余極限

要件

すべての数学スクリプトは次の方法でインストールされます：

uv sync

依存関係：sympy、z3-solver、numpy、scipy、mpmath、matplotlib、plotly