writing-lean-proofs plugin
Structured Lean 4 proof writing and library design following Mathlib conventions
How to install the writing-lean-proofs plugin
Run both commands inside Claude Code. The first adds the marketplace once; the second installs the plugin.
/plugin marketplace add trailofbits/skills
/plugin install writing-lean-proofs@trailofbitsWhat's inside writing-lean-proofs
1 part read from the plugin's own files.
Skills 1
Claude loads it when the task matches- writing-lean-proofs
Writes and reviews structured Lean 4 proofs and designs libraries following Mathlib conventions.
Using writing-lean-proofs in Claude Code
Skills need no command. Claude reads them when your request matches what they describe.
Update, turn off or remove
- Update the plugin (shell)
- claude plugin update writing-lean-proofs@trailofbits
- Refresh the marketplace
- /plugin marketplace update trailofbits
- Turn it off for now
- /plugin disable writing-lean-proofs@trailofbits
- Remove it
- /plugin uninstall writing-lean-proofs@trailofbits
Skills in writing-lean-proofs
- writing-lean-proofstrailofbits/skills
Writes and reviews structured Lean 4 proofs and designs libraries following Mathlib conventions.
9 files8.1Kstars
writing-lean-proofs plugin questions
How do I install the writing-lean-proofs plugin?
In Claude Code run /plugin marketplace add trailofbits/skills, then /plugin install writing-lean-proofs@trailofbits.
What does the writing-lean-proofs plugin include?
writing-lean-proofs bundles 1 skill.
How do I update or remove the writing-lean-proofs plugin?
Update it with claude plugin update writing-lean-proofs@trailofbits in your shell, or from the Installed tab of /plugin. Remove it with /plugin uninstall writing-lean-proofs@trailofbits.