prove

npx skills add majiayu000/claude-skill-registry --skill prove-carmandale-agent-config-2 --agent claude-code

Same command for any agent — swap --agent for codex, cursor, copilot.

# /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 b

Check if lake is available
command -v lake &>/dev/null && echo "Lean4 installed" || echo "Lean4 NOT installed"
Install elan (Lean version manager)
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
Restart shell, then verify
lake --version
loogle-search "pattern_here"
loogle-search "Nontrivial _ ↔ _"           # Find Nontrivial lemmas
loogle-search "(?a → ?b) → List ?a → List ?b"  # Map-like functions
loogle-search "IsCyclic, center"           # Multiple concepts