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…
Install
npx skills add trailofbits/skills --skill writing-lean-proofsnpx skills add trailofbits/skills --skill writing-lean-proofs -a claude-code -gnpx skills add trailofbits/skills --skill writing-lean-proofs -a codex -ggemini skills install https://github.com/trailofbits/skills.git --path plugins/writing-lean-proofs/skills/writing-lean-proofsgh skill install trailofbits/skills writing-lean-proofsgit clone --depth 1 https://github.com/trailofbits/skills /tmp/trailofbits__skills
mkdir -p ~/.claude/skills ~/.agents/skills
cp -R /tmp/trailofbits__skills/plugins/writing-lean-proofs/skills/writing-lean-proofs ~/.claude/skills/writing-lean-proofs # Claude Code
cp -R /tmp/trailofbits__skills/plugins/writing-lean-proofs/skills/writing-lean-proofs ~/.agents/skills/writing-lean-proofs # Codex, Cursor, Gemini CLI, Copilot, OpenCode