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).