domains / families / science / lean4-theorem-proving

lean4-theorem-proving

separate

Use when working with Lean 4 (.lean files), writing mathematical proofs, seeing "failed to synthesize instance" errors, managing sorry/axiom elimination, or searching mathlib for lemmas - provides build-first workflow, haveI/letI patterns, compiler-guided repair, and LSP integration

When to use

• Use for ANY Lean 4 development: pure/applied math, program verification, mathlib contributions. **Critical for:** Type class synthesis errors, sorry/axiom management, mathlib search, measure theory/probability work.

Skill page

Source