/writing-lean-proofs

name: writing-lean-proofs
description: "Writes and reviews structured Lean 4 proofs and designs Lean libraries following Mathlib conventions. Use when proving theorems in Lean, formalizing mathematics or specifications in Lean 4, defining new types or definitions in a Lean library, reviewing Lean proofs for readability and maintainability, refactoring long tactic proofs into lemmas, filling in sorry placeholders in a Lean development, setting up CI or linters for a Lean project, diagnosing slow proofs or maxHeartbeats timeouts, or writing custom tactics, macros, or linters."

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 ar