Agent skill · trailofbits
writing-lean-proofs
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.
What it needs
About 9k tokens when loaded.
What this skill does
Writing Lean Proofs Contents 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 (georgt linting, discretefield) 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. …
How to use it
Reference it in AdaL, Claude Code, Cursor or any coding agent — nothing to install:
@skills trailofbits/writing-lean-proofs