メニュー
Explain a proof or Lean code step-by-step for learning. Triggers on "explain", "how does this work", "teach me", "what does this mean", "walk me through", "I don't understand"
Codex または Claude でインストール この Prompt をコピーして Codex、Claude、または他のアシスタントに貼り付けると、Skill ページを確認してインストールできます。
SOC 職業分類に基づく
| name | explain-proof |
| description | Explain a proof or Lean code step-by-step for learning. Triggers on "explain", "how does this work", "teach me", "what does this mean", "walk me through", "I don't understand" |
Break down a proof into understandable pieces, explaining each step.
When explaining Lean tactics:
**What we're proving:** [goal in plain English]
**Current state:**
- We know: [hypotheses]
- We need: [goal]
**This step:** `tactic_name`
- What it does: [explanation]
- Why here: [reasoning]
- After this: [new goal/state]
| Tactic | Plain English |
|---|---|
intro h | "Assume the hypothesis, call it h" |
apply f | "Use theorem/function f" |
exact h | "This is exactly what h says" |
rw [h] | "Rewrite using equation h" |
simp | "Simplify using known facts" |
ring | "This follows by algebra" |
induction n | "Prove for 0, then prove n→n+1" |
cases h | "Consider all possibilities for h" |
constructor | "Prove both parts separately" |
left / right | "Prove one side of OR" |
obtain ⟨x, hx⟩ := h | "Unpack: h gives us x with property hx" |
**The claim:** [what we're proving]
**The approach:** [proof technique: direct, contradiction, induction, etc.]
**Key insight:** [the clever idea that makes it work]
**Step by step:**
1. [first step]
- Why: [justification]
2. [second step]
...
After each section:
After explaining, offer practice:
Ask early: "How familiar are you with [concept]?"
Explore a mathematical conjecture - gather evidence, find counterexamples, or build toward a proof. Triggers on "explore", "investigate", "what if", "is it true that", "find pattern", "check if"
Determine convergence or divergence of series using ratio test, root test, comparison test, and integral test. Triggers on "series converges", "test for convergence", "ratio test", "root test", "comparison test", "integral test", "sum of 1/n"
Prove geometric theorems using coordinate geometry. Convert shapes to algebraic expressions, use distance formula, midpoint formula, and slope calculations. Triggers on "prove using coordinates", "analytic geometry", "distance formula", "show collinear", "prove perpendicular", "prove parallel"
Prove identities or existence using combinatorial counting - double counting, bijections, inclusion-exclusion. Triggers on "count", "number of ways", "how many", "bijection", "one-to-one correspondence", "combinatorial proof"
Prove statements directly by assuming the hypothesis and deriving the conclusion through logical steps. Triggers on "prove directly", "show that", "demonstrate", "verify", "simple proof"
Prove limit statements using epsilon-delta definitions. Triggers on "epsilon-delta", "limit", "prove continuous", "show limit equals", "formal limit proof"