Writing Lean Proofs

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.

lean

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?

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.

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

have

lean

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

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

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 — definitions, APIs, bundling, abstraction boundaries, spec-driven project decomposition
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 — Mathlib naming so lemma names are computable from statements
anti-patterns.md — recognized anti-patterns, why each is harmful, and which linter catches it
llm-techniques.md — evidence-based techniques specific to LLM-written proofs
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 — measuring per-declaration cost, where reduction cost comes from, optimizing definitions without losing semantics
tactics.md — metaprogramming discipline: extension-point selection, metavariable and recovery safeguards, bounded search, actionable errors, structured tracing, generated declarations, and failure-surface testing

writing-lean-proofs

NPX Install

Tags

SKILL.md Content