domains / families / security / writing-lean-proofs

writing-lean-proofs

separate

Writes and reviews structured Lean 4 proofs and designs Lean libraries following Mathlib conventions. Use when proving theorems in Lean, formalizing mathematics or specifications in Lean 4, defining new types or definitions in a Lean library, reviewing Lean proofs for readability and maintainability, refactoring long tactic proofs into lemmas, filling in sorry placeholders in a Lean development, setting up CI or linters for a Lean project, diagnosing slow proofs or maxHeartbeats timeouts, or writing custom tactics, macros, or linters.

When to use

• Proving theorems in Lean 4, from single lemmas to multi-file developments
• Formalizing mathematics, protocols, or software specifications in Lean
• Defining new types, structures, or functions in a Lean library
• Reviewing Lean code for readability, maintainability, or Mathlib readiness
• Refactoring a long or fragile tactic proof into lemmas
• Setting up a formalization project that several people or agents will
• Setting up CI, linters, or verification gates for a Lean project — do this
• Diagnosing slow proofs, `maxHeartbeats` timeouts, or expensive reduction

When not to use

• Lean 4 as a general-purpose programming language (no proofs involved) —
• Coq, Isabelle, Agda, or Lean 3 — conventions and tactic names differ;
• Verified-software Lean projects with their own house style (e.g.

Skill page

Source