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.