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.

Jump to install

Repository: trailofbits/skills
Last source activity: August 7, 2026 at 20:23
Detected SKILL.md language: English
Stars: 6,567
Forks: 564

Install options

The review-first prompt is selected by default. You can switch to a direct command or download a local copy.

Install with Codex or Claude Copy this prompt, paste it into Codex, Claude, or another assistant, and let it review the skill page and install it for you.

A direct command skips the review prompt. Inspect the source before running it.

npx skills add https://github.com/trailofbits/skills --skill writing-lean-proofs

The command stays on one line. Scroll horizontally to inspect it before copying.

Prefer a local copy? Download the files currently available to SkillsMP.

Review the source files

Read SKILL.md and any companion files shown by SkillsMP before deciding whether to install.

File Explorer

9 files

SKILL.md

Source instructions · Read-only preview

Back to search Back to installation

codeql

Scans a codebase for security vulnerabilities using CodeQL's interprocedural data flow and taint tracking analysis. Triggers on "run codeql", "codeql scan", "build codeql database", "SAST scan", "taint analysis", "dataflow analysis", or "find vulnerabilities in this repo". Covers Python, JavaScript/TypeScript, Go, Java/Kotlin, C/C++, C#, Ruby, and Swift. Supports "run all" (security-and-quality + security-experimental) and "important only" (high-precision) scan modes, and creates data extension models for project-specific sources and sinks. For fast single-file pattern matching, or when no build is available for a compiled language, use the semgrep skill; to parse SARIF that already exists rather than produce it, use the sarif-parsing skill.

2026-08-11

supply-chain-risk-auditor

Audits a project's dependencies for supply-chain risk: version-matched advisories for direct dependencies and the full lockfile tree, abandoned or archived upstreams, npm publisher concentration, and install-time script execution. Use when asked to audit dependencies, assess supply-chain or third-party package risk, or review a dependency tree before an engagement.

2026-08-10

semgrep

Runs a Semgrep security scan over a codebase: detects languages, selects rulesets, presents the plan for explicit approval, then runs every approved ruleset through scripts/run-scans.sh, which batches the semgrep processes and writes scans.json, and merges the output to SARIF. Supports two scan modes, "run all" for full ruleset coverage and "important only" for security findings at medium-to-high confidence and impact. Uses Semgrep Pro for cross-file taint analysis when it is available. Use when asked to scan code for vulnerabilities, run a security audit with Semgrep, find bugs, or perform static analysis. For the same scan without the approval gate, use the /static-analysis:semgrep-scan workflow.

2026-08-10

View all from this repository

name

writing-lean-proofs

description

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

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

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.

writing-lean-proofs

Install options

Review the source files

Writing Lean Proofs

Contents

When to Use

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

writing-lean-proofs

Source facts

Install options

Review the source files

More from this repository

More from this repository

Writing Lean Proofs

Contents

When to Use

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