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:

# Check if lake is available
command -v lake &>/dev/null && echo "Lean4 installed" || echo "Lean4 NOT installed"

If 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

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)

   # 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)