Structured Lean 4 proof writing and library design, distilled from Mathlib's\nstyle and review conventions and from the methodology of large formalization\nprojects (Liquid Tensor Experiment, PFR, Fermat's Last Theorem).
\nCore principle: design top-down, prove bottom-up. Lean propositions are\nproof-irrelevant — only a theorem's statement can affect later declarations.\nStatements are the stable interface; proofs are disposable and freely\nreplaceable. Put design effort into definitions and statements, then fill in\nproofs against skeletons that already compile (modulo sorry).
maxHeartbeats timeouts, or expensive reductionge_or_gt linting, discrete_field) are obsoleteDefinitions carry the design weight. Before proving anything about a new\nconcept:
\nOption in\nsignatures (Mathlib: (0 : ℝ)⁻¹ = 0). Side conditions then appear only on\nthe lemmas that need them, not at every use site.FunLike instance;\nnew subobject kinds use SetLike; carry property proofs as structure\nfields, not separate IsHom-style predicates.ext, @[simp],\ncoercion, and injectivity lemmas — before the definition is used anywhere.\nDownstream proofs use the API, never unfold/show ... from rfl.See library-design.md for the full set of\ndesign rules with rationale.
\nState everything before proving anything, at every scale:
\n:= sorry, and make the file compile. Each sorry is now an\nindependent work unit — a contributor (human or LLM) can discharge one\nwithout understanding the rest. This is how LTE, PFR, and FLT scale to\ndozens of parallel contributors.have/suffices/calc\nskeleton with sorry justifications, get Lean to accept the structure,\nthen fill each step. Keeping the structure intact is what produces useful\nerror messages while you work.example (a b c d : ℝ) (h : c = d * a + b) (h' : b = a * d) : c = 2 * a * d := by\n calc\n c = d * a + b := sorry\n _ = d * a + a * d := sorry\n _ = 2 * a * d := sorry\n· with an indented block — never\nleave several goals active in unfocused sequence (Mathlib's multiGoal\nlinter enforces this). This is what kills fragile goal-ordering dependence.show stating its goal. The proof works\nwithout it; reviewers and future editors need it. If show would change\nthe goal, use change instead — keep stated goals honest.calc blocks, relations aligned\nvertically.have for forward stepping stones (\"we first establish X\"); suffices\nfor backward reduction (\"it suffices to show X\").trace_state at the point of interest or a deliberate done where goals\nshould be closed, then run lake env lean Path/To/File.lean; copy the\nreported hypotheses, case name, and target. Strip routine probes after the\nproof works. This is the single most effective technique for LLM-written\nproofs (see llm-techniques.md).See proof-style.md for the full tactic-style\nrules, and naming-conventions.md for\nnaming lemmas so their names are guessable from their statements.
\nDo not eyeball-check style — run the checkers. lake build is the floor,\nand it is only the floor: sorry is a warning, so a green build exits 0\nwith sorries still present.
#print axioms myTheorem for a spot check; for CI, collect axioms per\ndeclaration with Lean.collectAxioms and assert the whole expected\nfootprint ([propext, Classical.choice, Quot.sound] unless deliberately\nwidened), so a stray sorry or a new trust assumption like\nnative_decide fails loudly. Grep is wrong in both directions: it matches\nthe word in comments, and it misses a theorem whose own text is clean but\nwhich applies an unproved helper. Working script in\nlinting.md.linter.mathlibStandardSet wholesale in a downstream project: it\ncombines proof-maintenance checks with public-API checks, house style, and\nMathlib-specific repository policy. For a self-contained proof, start with\nlinter.auxLemma, linter.style.maxHeartbeats,\nlinter.style.multiGoal, linter.style.setOption, and\nlinter.style.show. A reusable library should additionally enable\nlinter.flexible, linter.style.missingEnd,\nlinter.style.openClassical, and the two unused*InType checks. Treat\nnativeDecide as a trust-policy choice and formatting or deprecated-syntax\nchecks as project style. No warning gates anything unless warnings fail\nthe build. Run Batteries' declaration-level #lint checks, including\nsimpNF, separately. Verify every option against the pinned Mathlib source\nand with a known-trigger fixture: a misspelled weak. option is\nintentionally ignored. The complete 26-member audit and lakefile profiles\nare in linting.md.@[env_linter] is one structure, and it is the only\nthing that reliably catches \"the attribute is missing on 29 of 30\ndeclarations\". See linting.md for the recipe and\nthe engineering rules (vacuity anchors, prove-it-can-fail, allowlists).When does proof structure graduate into separate lemmas?
\nBefore extracting, state the fragment's type and search by shape. Put\nthe proposed statement in a scratch example, run exact? and apply?\non the bare goal, then try a type-pattern and source search. If an existing\ntheorem fits, use it. Do not report an API gap without recording the\nsearches that failed.
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\n have h : ∀ x y : ℝ, min x y ≤ min y x := by\n intro x y\n apply le_min\n · show min x y ≤ y\n exact min_le_right x y\n · show min x y ≤ x\n exact min_le_left x y\n apply le_antisymm\n · show min a b ≤ min b a\n exact h a b\n · show min b a ≤ min a b\n exact h b a\nThe statement is independently interesting, or extraction sheds\nhypotheses the sub-argument does not need → standalone lemma. Dropping\nunneeded hypotheses is the stronger trigger: the extracted lemma becomes\nmore general than the proof it came from.
\nThe proof reads as \"long and unwieldy\" → split it. This is Mathlib's\nreview criterion, and it is deliberately qualitative — there is no line\nthreshold. Resolve doubt by attempting the extraction: if a fragment has\na clean statement, it wanted to be a lemma.
\n| Rule | \nWhy | \nEnforced by | \n
|---|---|---|
Never unfold definitions downstream; erw or trailing rfl = missing API | \nAPI lemmas are the abstraction boundary | \nreview (\"missing API\" smell) | \n
Terminal simp stays unsqueezed; non-terminal simp becomes simp only [...] | \nsqueezed terminal calls bury the key lemmas and break on renames | \nstyle guide | \n
One focused goal at a time (· blocks) | \nkills goal-ordering fragility | \nlinter.style.multiGoal | \n
show must not change the goal (use change) | \nstated goals stay honest | \nlinter.style.show | \n
No set_option debug/trace/profiler or unscoped maxHeartbeats in final code | \ndebugging scaffolding | \nlinter.style.setOption | \n
State lemmas in simp-normal form, < not > | \nsimp matches syntactically | \nsimpNF linter | \n
| Golf only when the result is at least as readable; trivial results exempt | \nshort ≠ better | \nreview | \n
Fact instances are local, never global | \nglobal instances degrade all typeclass search | \nreview | \n
| Name lemmas from their statements (see naming reference) | \nnames become guessable without search | \nlinter.style.nameCheck catches only __; #lint defsWithUnderscore and review cover more | \n
| Search a bare goal by shape before writing a helper or claiming an API gap | \nnames are not always guessable from the target | \nexact?, apply?, type/source search | \n
| Generally one tactic invocation per line; a one-line closing proof is the exception | \npreserves readable proof structure without inventing an absolute rule | \nstyle guide | \n
Gate sorry with collectAxioms/#print axioms, never grep | \ngrep matches comments, misses unproved helpers | \naxiom audit in CI | \n
| Prefer simp-lemma LHSs keyed on structure, not numerals; one spelling per constant | \n2 ^ 32 never matches a goal normalized to 4294967296 | \nsimpNF, review | \n
Re-derive every simp only list with simp? at its own site | \nlists do not transfer between look-alike goals | \nlinter.flexible | \n
Every maxHeartbeats override is an unproven claim — measure before believing | \ncopy-pasted budgets carry no information | \n#count_heartbeats, bisection | \n
Conditional simp lemma fires shallow but not deep → raise maxDischargeDepth (default 2) | \nchained side conditions truncate silently, no diagnostic | \ndiagnosis (proof-style, simp discipline) | \n
| Every project-specific convention gets a custom linter, in CI from day one | \nreview misses the 29-of-30 failure mode | \n@[env_linter] + #lint | \n
Full rationale for each row, plus the library-level anti-patterns, in\nanti-patterns.md.
\n| Excuse | \nReality | \n
|---|---|
| \"The proof compiles, ship it\" | \nCompiling 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. | \n
| \"Unfolding the definition is simpler than writing API lemmas\" | \nEvery downstream unfold couples a proof to the implementation. The first refactor breaks all of them at once. Write the missing lemma. | \n
| \"Squeezing every simp makes the proof faster and more robust\" | \nBackwards for terminal simp calls: the squeezed list breaks on every rename and drowns the signal. Squeeze non-terminal calls only. | \n
| \"It's shorter, therefore better\" | \nMathlib review policy: golfing is fine only when it does not sacrifice readability. Length is not the target; legibility is. | \n
| \"I'll restructure it into lemmas after it works\" | \nAfter it works, the structure is load-bearing and tangled. State the skeleton first; the lemmas fall out for free. | \n
\"Adding show lines is redundant noise\" | \nThey are redundant to the kernel and essential to every human or model that reads the proof next. | \n
| \"This helper is too specific to be a lemma\" | \nIf it has a clean statement, extract it — dropping the hypotheses it doesn't need usually reveals it was general all along. | \n
| \"We'll add linters once the library stabilizes\" | \nBackwards: 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. | \n
| \"The check passed, so we're clean\" | \nA 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. | \n
| \"The proof is slow, raise maxHeartbeats\" | \nAn 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. | \n