Writing Lean Proofs

Trail of BitsOfficialPublished by Trail of Bits

Skill
Tool integration
Software development
CC-BY-SA-4.0
No issues found

From the author

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.

— the description by Trail of Bits

AutoGineer summary

Written by AutoGineer from the skill’s own files, not by the author

This skill provides a rigorous methodology for formalizing mathematics and software specifications in Lean 4. It emphasizes a top-down design approach where definitions and API statements are established before proofs are written. By treating statements as stable interfaces and proofs as disposable, it enables scalable, parallel development. The skill covers the entire lifecycle of a Lean project, from initial sorry-based skeleton construction and API design to mechanical verification, linter configuration, and performance optimization.

What it does

Provides patterns for designing Lean 4 libraries and definitions.
Outlines a top-down workflow for building proof skeletons with sorry placeholders.
Defines best practices for proof structure, including calc blocks and focusing.
Details strategies for mechanical verification and CI integration.
Offers guidance on diagnosing performance issues and maxHeartbeats timeouts.
Provides rules for writing custom linters and macros.

When to use it

When starting a new formalization project in Lean 4.
When refactoring long, fragile tactic proofs into maintainable lemmas.
When designing new types or structures for a Lean library.
When setting up CI pipelines and linters for Lean projects.
When diagnosing slow proofs or unexpected timeouts.

Advantages

Promotes highly maintainable and readable proof code.
Enables parallel development through independent sorry-based work units.
Reduces technical debt by enforcing API-first design.
Provides clear, actionable criteria for proof extraction and refactoring.
Ensures project stability through automated linter and axiom verification.

Usage examples

“How should I structure a new Lean 4 library for group theory?”: The agent will advise defining the structures first, bundling properties using FunLike or SetLike, and writing the full API (ext, simp, coercion lemmas) in the same file before implementing any theorems.
“My proof is failing with a maxHeartbeats timeout. How do I fix it?”: The agent will guide you to measure the cost using #count_heartbeats, suggest decomposing the goal into smaller lemmas, or optimizing the definition's reduction behavior rather than simply increasing the budget.
“How can I ensure my Lean project is ready for multiple contributors?”: The agent will recommend creating a sorry-based skeleton, setting up a leanblueprint for dependency tracking, and configuring a strict CI environment with project-specific linters.

Install

Download the skill as a ZIP:
https://autogineer.com/agent-skills/trailofbits/writing-lean-proofs/download

Unzip it into the cross-client skills folder of your project:

mkdir -p .agents/skills && unzip writing-lean-proofs.zip -d .agents/skills

Documentation by Trail of Bits

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.

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.

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

Files

ATTRIBUTION.mdAdded by AutoGineer951 B
LICENSELicence file added by AutoGineer19.7 KiB
SKILL.md15.6 KiB
references/anti-patterns.md6.9 KiB
references/library-design.md7.7 KiB
references/linting.md22.1 KiB
references/llm-techniques.md5.4 KiB
references/naming-conventions.md2.5 KiB
references/performance.md5.3 KiB
references/proof-style.md7.8 KiB
references/tactics.md16.1 KiB

references/tactics.md

Writing tactics and metaprograms

Choose the smallest extension point
Define the tactic contract
Normalize inputs deliberately
Make speculative state transactional
Make failures local and actionable
Bound proof search
Build tracing in from the start
Generate syntax and declarations safely
Structure tactic code for change
Test the failure surface
Review checklist
Research sources

Custom tactics, macros, simprocs, and elaborators have distinctive failure modes. A bug can surface much later as a kernel error, silently leave automation in a partial state, or turn a fast failure into an unbounded search. Design the extension so invalid states are hard to create and every failure is attributable to one stage.

Choose the smallest extension point

Need	Prefer	Safeguard
Syntax-only expansion	hygienic `macro`	preserve syntax refs; avoid `unhygienic`
One local simplification step	simp lemma, `simproc`, or `dsimproc`	return `.continue` when inapplicable
Reusable goal-directed search	a scoped Aesop rule set	classify rules by semantic safety
Custom input elaboration or goal mutation	tactic elaborator	define state, failure, and goal-list contracts
Repeated low-level operation	typed `MetaM` helper	test it independently of parser syntax

Use ordinary lemmas before meta code. Recent Mathlib guidance treats simprocs as small steps in a larger simplification algorithm, not as general-purpose automation. Prefer Qq typed quotations for expression matching and proof construction when practical: raw Expr APIs allow ill-typed proof terms to exist until a later check.

Define the tactic contract

Before implementation, write down four observable outcomes:

Applicable and successful: which goals are closed or replaced, and in what order?
Inapplicable: is this an expected rule miss or a user-facing tactic error?
Malformed input: which syntax range receives which diagnostic?
Resource exhaustion or invariant failure: which error escapes, and what trace identifies the last completed phase?

An Aesop rule or simproc should normally fail softly when its pattern does not match. A tactic the user invoked directly should fail loudly when the target has the wrong shape. Never convert an internal invariant violation into a successful no-op.

Define success from the resulting goals, not from the helper's return value. A finishing tactic must leave no owned subgoals; a normalizer may leave one demonstrably changed goal. Tactics such as simp can return successfully after changing but not closing a goal, so wrap them in a terminal combinator when “finish” is part of the interface.

Preserve goals the tactic does not own. Use liftMetaTactic or replaceMainGoal for a tactic that transforms only the main goal; do not rebuild the whole goal list with setGoals unless reordering all goals is part of the documented contract.

Normalize inputs deliberately

Enter the goal context. Wrap tactic entry points in withMainContext, and run lower-level goal operations inside goal.withContext. Operations such as inferType and isDefEq need the correct local context; otherwise dependent local hypotheses become unknown free variables.
Do not pattern-match a stale expression. Use instantiateMVars before structural matching when assigned metavariables may remain in the expression. Use cleanupAnnotations when wrapper annotations are irrelevant, or whnfR when matching should unfold reducible definitions. Choose the weakest normalization that matches the tactic's stated semantics.
State the transparency mode. A tactic that happens to work under an ambient transparency setting is not stable. Pass the intended mode to matching, reduction, and unification helpers.
Finish elaboration checkpoints. After elaborating internal terms, use synthesizeSyntheticMVarsNoPostponing or an appropriate withSynthesize boundary. Otherwise a tactic can report success with pending coercion, typeclass, tactic, or postponed metavariables.
Assign only after a type check. Raw MVarId.assign skips occurs, scope, and type checks. Use assignIfDefeq, isDefEq against the metavariable type, or an elaborator such as elabTermEnsuringType that performs the check before assignment.
Prefer optional destructors over panics. A shape mismatch is ordinary for a rule. Prefer foo?, let some, and let_expr ... | return .continue over foo! and unreachable branches for inputs controlled by users or other tactics.

Make speculative state transactional

Unification and definitional equality checks can assign metavariables even when they look like queries. Treat every speculative branch as a transaction.

In MetaM, raw try/catch does not restore state. Use observing? for an optional result, withoutModifyingState for a read-only probe, or commitIfNoEx before a catch-and-fallback path.
In TacticM, exception handling backtracks tactic state. Do not expect the catch branch to see intermediate assignments or messages from the failed branch. If a diagnostic needs that state, collect it before failing or perform the narrow probe in MetaM/TermElabM with an explicit state contract.
Keep recovery scopes small. Wrap the one expected-to-fail probe, not the entire tactic. A broad catch can misclassify heartbeat exhaustion, recursion limits, or implementation bugs as “rule did not apply.”
Do not assume rollback erases everything. Caches, trace messages, and the global name generator are intentionally not fully backtracked. Traces should identify attempts without relying on generated names being reused.

Make failures local and actionable

Disable recovery for generated tactic syntax. If tactic code calls evalTactic on syntax it generated and expects to be correct, wrap the call in withoutRecover. Interactive recovery may otherwise log an error, insert sorry, and let the outer tactic appear to succeed.
Attach errors to the narrowest user syntax. Use withRef/withRef? around parsing and elaboration of an argument. Use throwTacticEx for a goal-specific failure so the diagnostic includes the tactic name and current goal.
Use MessageData, not pre-rendered strings, for Lean expressions. m!"{expr}" delaborates in context and remains readable; raw AST formatting usually hides the actual problem.
Name the failed phase and expectation. “Expected a target of the form P ∧ Q; got …” is repairable. “Tactic failed” is not. Distinguish input validation, normalization, candidate selection, proof construction, metavariable synthesis, and final assignment.
Do not swallow resource failures. If Lean cannot reliably distinguish an expected miss from a timeout in a broad handler, redesign the probe to return Option on ordinary misses and reserve exceptions for abnormal failures.

Bound proof search

Every loop needs a progress argument and a machine-checkable limit. Heartbeats alone are not a complete guard: a tactic can grow goals dramatically before hitting them, and some low-allocation loops are poor heartbeat clients.

Bound iterations, rule applications, recursion depth, generated candidates, and—where growth is possible—expression or goal size. Report which bound fired and include counters in the trace.
Make normalization loops prove progress with a decreasing or non-repeating measure. A rule that “succeeds” without changing the normalized state must not restart the loop.
In Aesop, mark a rule safe only if it preserves provability relative to the entire active rule set and is non-branching. A convenient rule is not automatically safe. Keep speculative choices unsafe so search can backtrack.
Scope expensive or aggressive rules to named rule sets. Do not put a domain-specific finishing tactic in the global default set where it will run on every unrelated goal.
Give optional fast paths a small local budget. A fail-soft fast path that consumes the ambient budget before falling back merely changes a quick failure into a slow one.
When search can emit a deterministic script (aesop?, simp?, or a custom suggestion), validate the emitted script before replacing the search call. Metavariable dependencies can make apparently harmless tactic reorderings change behavior.

Build tracing in from the start

Register a project-specific trace hierarchy with registerTraceClass; use trace[...] for leaves and withTraceNode for nested phases. Follow Lean's trace design rules:

Put the outcome in the collapsed top-level node.
Emit one child per phase or candidate decision, with rejection reasons only at deeper levels.
Record the input goal, normalized goal, active options/rule set, candidates tried, counters, and final subgoals or proof term. Keep the default view concise.
Use the caller's syntax ref so messages and trace nodes navigate to the relevant token.
Add a separate statistics trace for iteration counts, cache hits, goal size, and time. Do not make users infer a performance failure from thousands of low-level messages.

Keep dbg_trace, broad pp.all, and profiler options in local reproductions, not committed proof files. For proof-construction bugs, inspect what automation produced with show_term, by?, an Aesop proof trace, or the tactic's own final-proof trace. This separates “wrong search decision” from “right decision, malformed proof term.”

Generate syntax and declarations safely

Prefer hygienic quotations and antiquotations. Use unhygienic only when name capture is the explicit interface, and cover that behavior with tests.
Preserve source locations with quotations, withRef, mkIdentFrom, or mkIdentFromRef. Synthetic syntax whose ref spans a whole command produces unusable diagnostics and hover data.
Treat names as structured data. `foo ++ `bar is the dotted name foo.bar, not foo_bar. Build atomic generated names with Name.mkSimple on an explicitly constructed string.
Macro-generate repetitive lemma families, but verify the migration mechanically. For every old statement, compile an example proving that exact statement with the generated declaration under the calling convention downstream code uses. Also assert the expected declarations exist by name.

Structure tactic code for change

Separate parsing, normalization, search, proof construction, and goal mutation. Pure or narrowly stateful helpers are easier to test than one elaborator that performs every phase.
Extract shared cores from near-duplicate tactic families. Two ladders differing only in “recurse” versus “return” will drift when only one receives a new fast path or guard.
When two canonical variants are plausible, build the full proof suite both ways and record the result near the decision: which input failed, which invariant differed, and the measured cost.
An identity function at deliberate call sites may be a reserved normalization hook. Before deleting it, decide whether the call sites mark a stable phase boundary; if so, document the intended future invariant rather than leaving an unexplained no-op.
Verify dependency trigger conditions from source. “Runs only on failure” versus “runs on every call” changes an optimization from free to pay-per-call.

Test the failure surface

Test behavior, not private helper order. Every expected failure path needs a test that demonstrates both the diagnostic and the absence of state leakage.

Case	Assertion
Dependent local context	local variables remain in scope and generated terms type-check
Wrong target or malformed syntax	direct tactic fails at the relevant token with an actionable message
Rule or simproc miss	reports “not applicable” to its caller and leaves expression/state unchanged
Assigned metavariables, annotations, abbreviations	matching behavior follows the documented normalization
Multiple active goals	only owned goals change; remaining goal order is preserved
Pending synthetic metavariables	tactic completes synthesis or fails before reporting success
Non-terminal helper success	a finisher backtracks or fails if owned subgoals remain
Speculative branch mutates then fails	fallback observes the original metavariable and goal state
Looping or goal-growing rule	explicit bound fires and trace reports the responsible rule and counters
Generated proof or declaration family	exact old statements compile; negative fixtures are rejected
Trace disabled/enabled	default output stays quiet; trace identifies the failed phase and source ref

Use fail_if_success, guard_target, #check_failure, and #guard_msgs where appropriate. Include at least one known-trigger fixture: a checker or rule suite that is only tested on clean inputs can silently match zero items forever.

Review checklist

[ ] The extension point is no more powerful than the job requires.
[ ] Applicable, inapplicable, malformed, and exhausted outcomes are distinct.
[ ] Local context, normalization, transparency, and synthesis boundaries are explicit.
[ ] Every metavariable assignment is type-checked.
[ ] Every speculative mutation has rollback semantics and a narrow recovery scope.
[ ] Generated evalTactic syntax runs under withoutRecover.
[ ] Errors carry a source ref, tactic name, goal, phase, and expected shape.
[ ] Search has progress checks, explicit bounds, and scoped rules.
[ ] Opt-in traces show outcomes, decisions, counters, and final proof/subgoals.
[ ] Negative, state-leakage, multiple-goal, and pathological-growth tests exist.

Research sources

Community articles and guides:

Yaël Dillies and Paul Lezeau, Fantastic Simprocs and How to Write Them
Yaël Dillies and Paul Lezeau, Simp, made simple
Mathlib community, Metaprogramming gotchas
Lean community, Metaprogramming in Lean 4: MetaM and Tactics
Lean API documentation, trace messages and trace-class design

Forum discussions:

Kyle Miller on withoutRecover for generated evalTactic code
Eric Wieser and Kyle Miller on broad exception handling in tactics
Jannis Limperg and Sebastian Ullrich on diagnosing unbounded Aesop goal growth
Jannis Limperg on Aesop's safe-rule and debugging semantics

Papers by Lean tactic and metaprogramming developers:

Jannis Limperg and Asta Halkjær From, Aesop: White-Box Best-First Proof Search for Lean
Jannis Limperg, Tactic Script Optimisation for Aesop
Sebastian Ullrich and Leonardo de Moura, Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages
Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, and Leonardo de Moura, A Metaprogramming Framework for Formal Verification

Requirements and compatibility

Works with: Claude Code, Claude apps, OpenAI Codex, GitHub Copilot, Cursor, Gemini CLI, Kiro, OpenCode, Goose, Amp, Roo Code, JetBrains Junie, Factory Droid, Devin (ex-Windsurf), Mistral Vibe, OpenHands, Letta

“Works with” means the tool reads the open Agent Skills format; a skill written for one tool may use features others lack.

Security

No issues found by our static scan· No issues found

A static scan is not a guarantee. Skills are third-party content: review a skill before you let an agent use it.

Attribution and licence

Published by

Trail of Bits

Publisher

Trail of Bits (Official)

Source

trailofbits/skills · plugins/writing-lean-proofs/skills/writing-lean-proofs · commit e4dd0bb

Licence

Creative Commons Attribution-ShareAlike 4.0 International (redistribution allowed)

LICENSE (added by AutoGineer from LICENSE)
ATTRIBUTION.md (written by AutoGineer)

Synced

2026-11-09

AutoGineer is not affiliated with or endorsed by Trail of Bits or Trail of Bits.

Download ZIP

The ZIP holds the skill’s files, its licence files and an ATTRIBUTION.md. Download writing-lean-proofs.zip

From the author

AutoGineer summary

What it does

When to use it

Advantages

Usage examples

Install

Documentation by Trail of Bits

Writing Lean Proofs

Contents

When to Use

When NOT to Use

The workflow

1. Design definitions and their API first

2. Build a sorry skeleton

3. Fill goals, one focused goal at a time

4. Verify mechanically

The extraction ladder

Quick reference

Rationalizations to reject

References

Files

references/tactics.md

Writing tactics and metaprograms

Contents

Choose the smallest extension point

Define the tactic contract

Normalize inputs deliberately

Make speculative state transactional

Make failures local and actionable

Bound proof search

Build tracing in from the start

Generate syntax and declarations safely

Structure tactic code for change

Test the failure surface

Review checklist

Research sources

Requirements and compatibility

Security

Attribution and licence

Related skills

Implement

Source Driven Development

Write Swift

Cardputer Buddy

Typescript Pro

Scala Pro

Download ZIP