菜单
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 职业分类
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"
| 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]?"