prove

# /prove - Machine-Verified Proofs (5-Phase Workflow) **For mathematicians who want verified proofs without learning Lean syntax.** ## Prerequisites Before using this skill, check Lean4 is installed: ```bash # Check if lake is available command -v lake &>/dev/null && echo "Lean4 installed" || echo "Lean4 NOT installed" ``` **If not installed:** ```bash # Install elan (Lean version manager) curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh # Restart shell, then verify lake --version ``` First run of `/prove` will download Mathlib (~2GB) via `lake build`. ## Usage ``` /prove every group homomorphism preserves identity /prove Monsky's theorem /prove continuous functions on compact sets are uniformly continuous ``` ## The 5-Phase Workflow ``` ┌─────────────────────────────────────────────────────────────┐ │ 📚 RESEARCH → 🏗️ DESIGN → 🧪 TEST → ⚙️ IMPLEMENT → ✅ VERIFY │ └─────────────────────────────────────────────────────────────┘ ``` ### Phase 1: RESEARCH (before any Lean) **Goal:** Understand if/how this can be formalized. 1. **Search Mathlib with Loogle** (PRIMARY - type-aware search) ```bash # Use loogle for type signature search - finds lemmas by shape loogle-search "pattern_here" # Examples: loogle-search "Nontrivial _ ↔ _" # Find Nontrivial lemmas loogle-search "(?a → ?b) → List ?a → List ?b" # Map-like functions loogle-search "IsCyclic, center" # Multiple concepts ``` **Query syntax:** - `_` = any single type - `?a`, `?b` = type variables (same var = same type) - `Foo, Bar` = must mention both 2. **Search External** - What's the known proof strategy? - Use Nia MCP if available: `mcp__nia__search` - Use Perplexity MCP if available: `mcp__perplexity__search` - Fall back to WebSearch for papers/references - Check: Is there an existing formalization elsewhere (Coq, Isabelle)? 3. **Identify Obstacles** - What lemmas are NOT in Mathlib? - Does proof require axioms beyond ZFC? (Choice, LEM, etc.) - Is the statement even true? (search for counterexamples) 4. **Output:** Brief summary of proof strategy and obstacles **CHECKPOINT:** If obstacles found, use AskUserQuestion: - "This requires [X]. Options: (a) restricted version, (b) accept axiom, (c) abort" ### Phase 2: DESIGN (skeleton with sorries) **Goal:** Build proof structure before filling details. 1. Create Lean file with: - Imports - Definitions needed - Main theorem statement - Helper lemmas as `sorry` 2. Annotate each sorry: ```lean -- SORRY: needs proof (straightforward) -- SORRY: needs proof (complex - ~50 lines) -- AXIOM CANDIDATE: v₂ constraint - will test in Phase 3 ``` 3. Verify skeleton compiles (with sorries) **Output:** `proofs/<theorem_name>.lean` with annotated structure ### Phase 3: TEST (counterexample search) **Goal:** Catch false lemmas BEFORE trying to prove them. For each AXIOM CANDIDATE sorry: 1. **Generate test cases** ```lean -- Create #eval or example statements #eval testLemma (randomInput1) -- should return true #eval testLemma (randomInput2) -- should return true ``` 2. **Run tests** ```bash lake env lean test_lemmas.lean ``` 3. **If counterexample found:** - Report the counterexample - Use AskUserQuestion: "Lemma is FALSE. Options: (a) restrict domain, (b) reformulate, (c) abort" **CHECKPOINT:** Only proceed if all axiom candidates pass testing. ### Phase 4: IMPLEMENT (fill sorries) **Goal:** Complete the proofs. Standard iteration loop: 1. Pick a sorry 2. Write proof attempt 3. Compiler-in-the-loop checks (hook fires automatically) 4. If error, Godel-Prover suggests fixes 5. Iterate until sorry is filled 6. Repeat for all sorries **Tools active:** - compiler-in-the-loop hook (on every Write) - Godel-Prover suggestions (on errors) ### Phase 5: VERIFY (audit) **Goal:** Confirm proof quality. 1. **Axiom Audit** ```bash lake build && grep "depends on axioms" output ``` - Standard: propext, Classical.choice, Quot.sound ✓ - Custom axioms: LIST EACH ONE 2. **Sorry Count** ```bash grep -c "sorry" proofs/<file>.lean ``` - Must be 0 for "complete" proof 3. **Generate Summary** ``` ✓ MACHINE VERIFIED (or ⚠️ PARTIAL - N axioms) Theorem: <statement> Proof Strategy: <brief description> Proved: - <lemma 1> - <lemma 2> Axiomatized (if any): - <axiom>: <why it's needed> File: proofs/<name>.lean ``` ## Research Tool Priority Use whatever's available, in order: | Tool | Best For | Command | |------|----------|---------| | **Loogle** | Type signature search (PRIMARY) | `loogle-search "pattern"` | | Nia MCP | Library documentation | `mcp__nia__search` | | Perplexity MCP | Proof strategies, papers | `mcp__perplexity__search` | | WebSearch | General references | WebSearch tool | | WebFetch | Specific paper/page content | WebFetch tool | **Loogle setup:** Requires `~/tools/loogle` with Mathlib index. Run `loogle-server &` for fast queries. If no search tools available, proceed with caution and note "research phase skipped". ## Checkpoints (automatic) The workflow pauses for user input when: - ⚠️ Research finds obstacles - ❌ Testing finds counterexamples - 🔄 Implementation hits unfillable sorry after N attempts ## Output Format ``` ┌─────────────────────────────────────────────────────┐ │ ✓ MACHINE VERIFIED │ │ │ │ Theorem: ∀ φ : G →* H, φ(1_G) = 1_H │ │ │ │ Proof Strategy: Direct application of │ │ MonoidHom.map_one from Mathlib. │ │ │ │ Phases: │ │ 📚 Research: Found in Mathlib.Algebra.Group.Hom │ │ 🏗️ Design: Single lemma, no sorries needed │ │ 🧪 Test: N/A (trivial) │ │ ⚙️ Implement: 3 lines │ │ ✅ Verify: 0 custom axioms, 0 sorries │ │ │ │ File: proofs/group_hom_identity.lean │ └─────────────────────────────────────────────────────┘ ``` ## What I Can Prove | Domain | Examples | |--------|----------| | Category Theory | Functors, natural transformations, Yoneda | | Abstract Algebra | Groups, rings, homomorphisms | | Topology | Continuity, compactness, connectedness | | Analysis | Limits, derivatives, integrals | | Logic | Propositional, first-order | ## Limitations - Complex proofs may take multiple iterations - Novel research-level proofs may exceed capabilities - Some statements are unprovable over ℚ (need ℝ extension) ## Behind The Scenes - **Lean 4.26.0** - Theorem prover - **Mathlib** - 100K+ formalized theorems - **Godel-Prover** - AI tactic suggestions (via LMStudio) - **Compiler-in-the-loop** - Automatic verification on every write - **Research tools** - Nia, Perplexity, WebSearch (graceful degradation) ## See Also - `/loogle-search` - Search Mathlib by type signature (used in Phase 1 RESEARCH) - `/math-router` - For computation (integrals, equations) - `/lean4` - Direct Lean syntax access