/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 will download Mathlib ( 2GB) via . 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 - , = type variables (same var = same type) - = must mention both 2. Search External - What's the known proof strategy? - Use Nia MCP if…