lean4
Lean 4 Theorem Proving
Use this skill whenever you're editing Lean 4 proofs, debugging Lean builds, formalizing mathematics in Lean, or learning Lean 4 concepts. It prioritizes LSP-based inspection and mathlib search, with scripted primitives for sorry analysis, axiom checking, and error parsing.
Core Principles
Search before prove. Many mathematical facts already exist in mathlib. Search exhaustively before writing tactics.
Build incrementally. Lean's type checker is your test suite—if it compiles with no sorries and standard axioms only, the proof is sound.
Respect scope. Follow the user's preference: fill one sorry, its transitive dependencies, all sorries in a file, or everything. Ask if unclear.
Use 100-character line width for Lean files. Do not wrap lines at 80 characters — Lean and mathlib convention is 100. If a line fits within 100 characters, keep it on one line. See mathlib-style for breaking strategies when lines exceed 100.
Mathlib style quick check. For ordinary mathematical lambdas, write fun x ↦ ... (\mapsto), not fun x => .... Use => for match/do branches and metaprogramming callback idioms. Prefer show P by tac for tactic proofs; use show P from term only for term proofs. See mathlib-style.
Preserve statements, signatures, and docstrings — they're the file's API. Theorem/lemma statements, type signatures, and docstrings are off-limits unless the user explicitly requests changes; changing them can break callers or alter the theorem being proved. Inline comments may be adjusted, but docstrings may not. If a proof seems to require changing a statement or adding a custom axiom, stop and discuss first because that changes the contract or the proof's trust basis. Exception: within synthesis wrappers (/lean4:formalize, /lean4:autoformalize), session-generated declarations may be redrafted under the outer-loop statement-safety rules; see cycle-engine.md.