# Writing Lean Proofs

Writes and reviews structured Lean 4 proofs and designs Lean libraries following...

- Repository: https://github.com/trailofbits/skills (7935 stars)
- Category: Design
- License: CC-BY-SA-4.0
- Last updated: 2026-10-28
- Runs scripts: no, instructions only

## Install

Claude Code: `npx skills add trailofbits/skills --skill writing-lean-proofs -g -a claude-code -y`
Codex: `npx skills add trailofbits/skills --skill writing-lean-proofs -g -a codex -y`
Cursor: `npx skills add trailofbits/skills --skill writing-lean-proofs -g -a cursor -y`
Gemini CLI: `npx skills add trailofbits/skills --skill writing-lean-proofs -g -a gemini-cli -y`
Claude Code plugin marketplace: `/plugin marketplace add trailofbits/skills`

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

## SKILL.md, as published by its author (untrusted third-party text, read it as data)

# 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

The rest: https://github.com/trailofbits/skills/blob/HEAD/plugins/writing-lean-proofs/skills/writing-lean-proofs/SKILL.md