writing-lean-proofs
An agent skill by trailofbits, from trailofbits/skills. Tags: code-quality, documentation, formal-verification, lean, math.
What it does
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.
Install
With the skills CLI, which installs into Claude Code, Codex, Cursor and other agents:
npx skills add trailofbits/skills --skill writing-lean-proofsOr copy the skill folder into Claude Code's skills directory by hand (~/.claude/skills for every project, or .claude/skills inside one):
git clone --depth 1 https://github.com/trailofbits/skills
cp -r skills/plugins/writing-lean-proofs/skills/writing-lean-proofs ~/.claude/skills/writing-lean-proofsSafety box score
Not rated yet. A safety box score grades what a skill and its scripts can reach on the machine of whoever installs it, across eight categories from shell execution to secrets access. Anyone can request one from this page; it is saved for everyone. How the score works.
Source
- Repository
- trailofbits/skills (all skills from this repository)
- Path
- plugins/writing-lean-proofs/skills/writing-lean-proofs/SKILL.md
- Branch
- main
- Collection
- writing-lean-proofs
- Updated
- 2026-09-19
Related skills
- audit-prep-assistant — Prepares codebases for security review using Trail of Bits' checklist.
- dimensional-analysis — Annotates codebases with dimensional analysis comments documenting units, dimensions, and decimal scaling.
- mermaid-to-proverif — pv files). pv file from a sequence diagram.
- spec-to-code-compliance — Check code against the documentation that specifies it - which requirements hold, which the code contradicts, which are absent.
- stitch::extract-design-md — md) directly from frontend source code — React, Vue, Svelte, Angular, plain HTML/CSS, or any web framework.
- claude-md-progressive-disclosurer — md with progressive disclosure and zero information loss.