Writing Lean Proofs

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

• Lean 4 as a general-purpose programming language (no proofs involved) — most of this skill targets proof and API structure
• Coq, Isabelle, Agda, or Lean 3 — conventions and tactic names differ; Lean 3 idioms (ge_or_gt linting, discrete_field) are obsolete
• Verified-software Lean projects with their own house style (e.g. spec-traceability-first codebases): Mathlib conventions are the community default, but check the project's CONTRIBUTING first and defer to it

The workflow

1. Design definitions and their API first

Definitions carry the design weight. Before proving anything about a new concept:

• Prefer total functions with junk values over subtypes or Option in signatures (Mathlib: (0 : ℝ)⁻¹ = 0). Side conditions then appear only on the lemmas that need them, not at every use site.
• Bundle: new morphism kinds are structures with a FunLike instance; new subobject kinds use SetLike; carry property proofs as structure fields, not separate IsHom-style predicates.
• Pick the canonical spelling (simp-normal form) for every concept with multiple equivalent forms, and state all API lemmas for that form only.
• Write the API in the same file, immediately: ext, @[simp], coercion, and injectivity lemmas — before the definition is used anywhere. Downstream proofs use the API, never unfold/show ... from rfl.

See library-design.md for the full set of design rules with rationale.

2. Build a sorry skeleton

State everything before proving anything, at every scale:

• Project scale: state the target theorem and the lemmas it needs, all with := sorry, and make the file compile. Each sorry is now an independent work unit — a contributor (human or LLM) can discharge one without understanding the rest. This is how LTE, PFR, and FLT scale to dozens of parallel contributors.
• Proof scale: inside a proof, lay out the have/suffices/calc skeleton with sorry justifications, get Lean to accept the structure, then fill each step. Keeping the structure intact is what produces useful error messages while you work.

example (a b c d : ℝ) (h : c = d * a + b) (h' : b = a * d) : c = 2 * a * d := by
  calc
    c = d * a + b     := sorry
    _ = d * a + a * d := sorry
    _ = 2 * a * d     := sorry

3. Fill goals, one focused goal at a time

• Every new subgoal gets a focusing dot · with an indented block — never leave several goals active in unfocused sequence (Mathlib's multiGoal linter enforces this). This is what kills fragile goal-ordering dependence.
• Open each block with a redundant show stating its goal. The proof works without it; reviewers and future editors need it. If show would change the goal, use change instead — keep stated goals honest.
• Chained rewrites of (in)equalities become calc blocks, relations aligned vertically.
• have for forward stepping stones ("we first establish X"); suffices for backward reduction ("it suffices to show X").
• While drafting, annotate the goal state as a comment before non-obvious tactics — emitted by Lean, never imagined. In a headless workflow, insert trace_state at the point of interest or a deliberate done where goals should be closed, then run lake env lean Path/To/File.lean; copy the reported hypotheses, case name, and target. Strip routine probes after the proof works. This is the single most effective technique for LLM-written proofs (see llm-techniques.md).

See proof-style.md for the full tactic-style rules, and naming-conventions.md for naming lemmas so their names are guessable from their statements.

4. Verify mechanically

Do not eyeball-check style — run the checkers. lake build is the floor, and it is only the floor: sorry is a warning, so a green build exits 0 with sorries still present.

• Gate unproved obligations by asking the kernel, never by grepping. #print axioms myTheorem for a spot check; for CI, collect axioms per declaration with Lean.collectAxioms and assert the whole expected footprint ([propext, Classical.choice, Quot.sound] unless deliberately widened), so a stray sorry or a new trust assumption like native_decide fails loudly. Grep is wrong in both directions: it matches the word in comments, and it misses a theorem whose own text is clean but which applies an unproved helper. Working script in linting.md.
• Choose lints by project role and put them in CI at project start. Do not enable linter.mathlibStandardSet wholesale in a downstream project: it combines proof-maintenance checks with public-API checks, house style, and Mathlib-specific repository policy. For a self-contained proof, start with linter.auxLemma, linter.style.maxHeartbeats, linter.style.multiGoal, linter.style.setOption, and linter.style.show. A reusable library should additionally enable linter.flexible, linter.style.missingEnd, linter.style.openClassical, and the two unused*InType checks. Treat nativeDecide as a trust-policy choice and formatting or deprecated-syntax checks as project style. No warning gates anything unless warnings fail the build. Run Batteries' declaration-level #lint checks, including simpNF, separately. Verify every option against the pinned Mathlib source and with a known-trigger fixture: a misspelled weak. option is intentionally ignored. The complete 26-member audit and lakefile profiles are in linting.md.
• Write a custom linter for every project-specific convention (simp-set discipline, summary-lemma coverage, required attributes) — a declaration-level @[env_linter] is one structure, and it is the only thing that reliably catches "the attribute is missing on 29 of 30 declarations". See linting.md for the recipe and the engineering rules (vacuity anchors, prove-it-can-fail, allowlists).

The extraction ladder

When does proof structure graduate into separate lemmas?

0. Before extracting, state the fragment's type and search by shape. Put the proposed statement in a scratch example, run exact? and apply? on the bare goal, then try a type-pattern and source search. If an existing theorem fits, use it. Do not report an API gap without recording the searches that failed.

1. A sub-argument repeats within one proof → name it as a local have.

   theorem min_comm (a b : ℝ) : min a b = min b a := by
     have h : ∀ x y : ℝ, min x y ≤ min y x := by
       intro x y
       apply le_min
       · show min x y ≤ y
         exact min_le_right x y
       · show min x y ≤ x
         exact min_le_left x y
     apply le_antisymm
     · show min a b ≤ min b a
       exact h a b
     · show min b a ≤ min a b
       exact h b a

2. The statement is independently interesting, or extraction sheds hypotheses the sub-argument does not need → standalone lemma. Dropping unneeded hypotheses is the stronger trigger: the extracted lemma becomes more general than the proof it came from.

3. The proof reads as "long and unwieldy" → split it. This is Mathlib's review criterion, and it is deliberately qualitative — there is no line threshold. Resolve doubt by attempting the extraction: if a fragment has a clean statement, it wanted to be a lemma.