/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: If not installed: First run of /prove will download Mathlib (~2GB) via lake build . Usage The 5 Phase Workflow Phase 1: RESEARCH (before any Lean) Goal: Understand if/how this can be formalized. 1. Search Mathlib with Loogle (PRIMARY type aware search) 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: 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 2. Run tests 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 Standard: propext, Classical.choice, Quot.sound ✓ Custom axioms: LIST EACH ONE 2. Sorry Count Must be 0 for "complete" proof 3. Generate Summary 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 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