writing-lean-proofs — Claude Code skill for Lean 4
Guides Lean 4 proof writing and review using Mathlib conventions. Use it when formalising theorems, restructuring tactic code, or adding project checks.
npx skills add trailofbits/skills --skill writing-lean-proofs -a claude-codeWhat writing-lean-proofs does
The skill starts with declarations and theorem statements, then works down to proofs. It encourages compiling a skeleton with sorry, isolating each goal, and using calc for equality chains. It also distinguishes forward helper facts with have from backward reductions with suffices.
It covers APIs around new definitions, including ext, @[simp], coercion, and injectivity lemmas. For proof-state inspection, it uses trace_state, done, and lake env lean Path/To/File.lean. It also addresses slow proof terms and maxHeartbeats timeouts.
Its guidance follows Mathlib practice. If a Lean project has its own CONTRIBUTING rules, check those first; that matters more than applying this style unchanged. The skill is aimed at Lean 4 rather than Lean 3, Coq, Isabelle, or Agda.
What it helps with
- split a Lean 4 proof into separate lemmas
- replace
sorryplaceholders in a development - refactor a long tactic proof into
calcsteps - diagnose a
maxHeartbeatstimeout - add CI checks for unproved obligations
Example prompts for the agent
- “Create a Lean 4 proof skeleton for this theorem and leave separate steps as
sorry.” - “Review this Lean file against Mathlib conventions and identify lemmas to extract.”
- “Investigate the
maxHeartbeatstimeout inPath/To/File.leanusingtrace_state.”
How to install writing-lean-proofs
1Skills CLI (Vercel)
npx skills add trailofbits/skills --skill writing-lean-proofs -a claude-code2Manually: put the files in place
~/.claude/skills/writing-lean-proofs/SKILL.mdCopy the whole skill folder; for one project use .claude/skills/writing-lean-proofs/
1Skills CLI (Vercel)
npx skills add trailofbits/skills --skill writing-lean-proofs -a codex2Manually: put the files in place
.agents/skills/writing-lean-proofs/SKILL.mdFor all projects use ~/.agents/skills/
1Skills CLI (Vercel)
npx skills add trailofbits/skills --skill writing-lean-proofs -a cursor2Manually: put the files in place
.cursor/skills/writing-lean-proofs/SKILL.mdCursor also reads .agents/skills/ and .claude/skills/
1GitHub CLI
gh skill install trailofbits/skills writing-lean-proofs2Manually: put the files in place
.github/skills/writing-lean-proofs/SKILL.md1Skills CLI (Vercel)
npx skills add trailofbits/skills --skill writing-lean-proofs -a gemini-cli2Platform CLI
gemini skills install https://github.com/trailofbits/skills --path plugins/writing-lean-proofs/skills/writing-lean-proofsManually: put the files in place
.devin/skills/writing-lean-proofs/SKILL.mdThe legacy .windsurf/skills/ path still works
Skills CLI (Vercel)
npx skills add trailofbits/skills --skill writing-lean-proofs -a opencodeClaude.ai
Zip the folder and upload it in Settings → Capabilities → Skills
Step by step, with commands for each platform: How to install skills in Claude Code: five ways
Questions about writing-lean-proofs
How do I install writing-lean-proofs in Claude Code?
Run npx skills add trailofbits/skills --skill writing-lean-proofs -a claude-code, then run npx skills add trailofbits/skills --skill writing-lean-proofs -a claude-code again. The skill file is at ~/.claude/skills/writing-lean-proofs/SKILL.md.
What does writing-lean-proofs do?
It guides the design, writing, review, and refactoring of Lean 4 proofs using Mathlib-oriented practices. It also covers linters and CI verification work.
Does writing-lean-proofs support Lean 3?
No. Its conventions target Lean 4, and Lean 3 uses different tactics and idioms.
