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
code
**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
code
**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