writing-lean-proofs

Writing Lean Proofs

Contents

• [When to Use](#when-to-use)
• [When NOT to Use](#when-not-to-use)
• [The workflow](#the-workflow)
• [The extraction ladder](#the-extraction-ladder)
• [Quick reference](#quick-reference)
• [Rationalizations to reject](#rationalizations-to-reject)
• [References](#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](references/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](references/llm-techniques.md)).

See [proof-style.md](references/proof-style.md) for the full tactic-style

rules, and [naming-conventions.md](references/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](references/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](references/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](references/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?

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

1. **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.

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

Quick reference

| Rule | Why | Enforced by |

|------|-----|-------------|

| Never unfold definitions downstream; erw or trailing rfl = missing API | API lemmas are the abstraction boundary | review ("missing API" smell) |

| Terminal simp stays unsqueezed; non-terminal simp becomes simp only [...] | squeezed terminal calls bury the key lemmas and break on renames | style guide |

| One focused goal at a time (· blocks) | kills goal-ordering fragility | linter.style.multiGoal |

| show must not change the goal (use change) | stated goals stay honest | linter.style.show |

| No set_option debug/trace/profiler or unscoped maxHeartbeats in final code | debugging scaffolding | linter.style.setOption |

| State lemmas in simp-normal form, < not > | simp matches syntactically | simpNF linter |

| Golf only when the result is at least as readable; trivial results exempt | short ≠ better | review |

| Fact instances are local, never global | global instances degrade all typeclass search | review |

| Name lemmas from their statements (see naming reference) | names become guessable without search | linter.style.nameCheck catches only __; #lint defsWithUnderscore and review cover more |

| Search a bare goal by shape before writing a helper or claiming an API gap | names are not always guessable from the target | exact?, apply?, type/source search |

| Generally one tactic invocation per line; a one-line closing proof is the exception | preserves readable proof structure without inventing an absolute rule | style guide |

| Gate sorry with collectAxioms/#print axioms, never grep | grep matches comments, misses unproved helpers | axiom audit in CI |

| Prefer simp-lemma LHSs keyed on structure, not numerals; one spelling per constant | 2 ^ 32 never matches a goal normalized to 4294967296 | simpNF, review |

| Re-derive every simp only list with simp? at its own site | lists do not transfer between look-alike goals | linter.flexible |

| Every maxHeartbeats override is an unproven claim — measure before believing | copy-pasted budgets carry no information | #count_heartbeats, bisection |

| Conditional simp lemma fires shallow but not deep → raise maxDischargeDepth (default 2) | chained side conditions truncate silently, no diagnostic | diagnosis (proof-style, simp discipline) |

| Every project-specific convention gets a custom linter, in CI from day one | review misses the 29-of-30 failure mode | @[env_linter] + #lint |

Full rationale for each row, plus the library-level anti-patterns, in

[anti-patterns.md](references/anti-patterns.md).

Rationalizations to reject

| Excuse | Reality |

|--------|---------|

| "The proof compiles, ship it" | Compiling is the floor. A monolithic tactic block that only Lean can read will break silently at the next Mathlib bump and no one will be able to repair it. |

| "Unfolding the definition is simpler than writing API lemmas" | Every downstream unfold couples a proof to the implementation. The first refactor breaks all of them at once. Write the missing lemma. |

| "Squeezing every simp makes the proof faster and more robust" | Backwards for terminal simp calls: the squeezed list breaks on every rename and drowns the signal. Squeeze non-terminal calls only. |

| "It's shorter, therefore better" | Mathlib review policy: golfing is fine only when it does not sacrifice readability. Length is not the target; legibility is. |

| "I'll restructure it into lemmas after it works" | After it works, the structure is load-bearing and tangled. State the skeleton first; the lemmas fall out for free. |

| "Adding show lines is redundant noise" | They are redundant to the kernel and essential to every human or model that reads the proof next. |

| "This helper is too specific to be a lemma" | If it has a clean statement, extract it — dropping the hypotheses it doesn't need usually reveals it was general all along. |

| "We'll add linters once the library stabilizes" | Backwards: patterns propagate by copy-paste, so a deferred linter meets a 400-warning backlog instead of one bad line. Enable what is already clean and gate it now. |

| "The check passed, so we're clean" | A check that can't fail proves nothing — sweeps reach zero files, misspelled weak. options are ignored, pipelines swallow exit codes. Prove every gate can fail before trusting that it passes. |

| "The proof is slow, raise maxHeartbeats" | An unmeasured budget is a claim, not a fix — and it masks the regression the next reader needs to see. Measure with #count_heartbeats; restructure the definition or decompose the goal. |

References

• [library-design.md](references/library-design.md) — definitions, APIs,

bundling, abstraction boundaries, spec-driven project decomposition

• [proof-style.md](references/proof-style.md) — tactic proof structure:

calc, have/suffices, focusing, and simp discipline including the

why-doesn't-this-lemma-fire diagnoses (discharge depth, traversal order,

numeral spellings)

• [naming-conventions.md](references/naming-conventions.md) — Mathlib naming

so lemma names are computable from statements

• [anti-patterns.md](references/anti-patterns.md) — recognized anti-patterns,

why each is harmful, and which linter catches it

• [llm-techniques.md](references/llm-techniques.md) — evidence-based

techniques specific to LLM-written proofs

• [linting.md](references/linting.md) — axiom-based sorry gates, enabling

project-specific linter profiles in CI early, the full Mathlib standard-set

audit, adopting linters with a backlog, writing custom linters for

project-specific constructs, and proving every gate can fail

• [performance.md](references/performance.md) — measuring per-declaration

cost, where reduction cost comes from, optimizing definitions without

losing semantics

• [tactics.md](references/tactics.md) — metaprogramming discipline:

extension-point selection, metavariable and recovery safeguards, bounded

search, actionable errors, structured tracing, generated declarations,

and failure-surface testing