Prove

This is a structured workflow for getting machine-verified proofs in Lean4 without needing to know Lean syntax. It walks through five phases: research (using Loogle to search Mathlib by type signature), design (building a skeleton with sorries), testing (catching false lemmas with counterexamples), implementation (filling in proofs with compiler-in-the-loop feedback), and verification (axiom audit). The research phase is notably thorough, checking multiple sources and identifying obstacles before writing any code. Use this when you need formal verification of mathematical statements and want guardrails against common mistakes like trying to prove false lemmas. The checkpoint system pauses for user input when it hits roadblocks, which is honest about what automated proving can and cannot handle.

skills.sh installs: 508
GitHub stars: 3.9K
last updated: Aug 21, 2026

View on GitHub

Install

$ npx -y skills add parcadei/continuous-claude-v3 --skill prove --agent claude-code

Installs into .claude/skills of the current project.

Files

/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  │
└─────────────────────────────────────────────────────────────┘