Writing Lean Proofs

Contents

• When to Use
• When NOT to Use
• The workflow
• The extraction ladder
• Quick reference
• Rationalizations to reject
• References

Structured Lean 4 proof writing and library design, distilled from Mathlib's style and review conventions and from the methodology of large formalization projects (Liquid Tensor Experiment, PFR, Fermat's Last Theorem).

Core principle: design top-down, prove bottom-up. Lean propositions are proof-irrelevant, only a theorem's statement can affect later declarations. Statements are the stable interface; proofs are disposable and freely replaceable. Put design effort into definitions and statements, then fill in proofs against skeletons that already compile (modulo sorry).

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 contribute to in parallel
• Setting up CI, linters, or verification gates for a Lean project, do this at project start, before patterns propagate
• Diagnosing slow proofs, maxHeartbeats timeouts, or expensive reduction
• Writing custom tactics, macros, or project-specific linters

When NOT to Use