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 ``` **Q...