| 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" |
Explain Proof
Break down a proof into understandable pieces, explaining each step.
Approach
- Start with the big picture
- Break into chunks
- Explain each chunk in plain language
- Connect to the formal notation
- Check understanding before continuing
For Lean Code
When explaining Lean tactics:
Structure
**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]
Common Tactics Explained
| 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" |
For Informal Proofs
Structure
**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]
...
Interactive Elements
After each section:
- "Does this make sense so far?"
- "Want me to go deeper on any part?"
- "Ready to try a similar example?"
Exercises
After explaining, offer practice:
- Predict what the next tactic should be
- Fill in a missing step
- Prove a similar theorem
- Explain a step back to me
Adapting to Level
Ask early: "How familiar are you with [concept]?"
- Beginner: More analogies, less notation
- Intermediate: Balance of intuition and rigor
- Advanced: Focus on subtle points, skip basics
