← Browse
writing-lean-proofs
trailofbits ★ 7875
A Claude Code plugin that guides structured Lean 4 proof writing following Mathlib conventions, using a design-first, prove-bottom-up workflow with sorry skeletons and mechanical verification. It includes comprehensive references on library design, proof style, naming, anti-patterns, LLM-specific techniques, and linting, plus an evaluation suite with planted bugs for testing review workflows.
Install
> /plugin marketplace add trailofbits/skills/tree/HEAD/plugins/writing-lean-proofs
> /plugin install writing-lean-proofs
Source: https://github.com/trailofbits/skills/tree/HEAD/plugins/writing-lean-proofs
What it's made of
1 skill
- Commands
- 0
- Agents
- 0
- Skills
- 1
- MCP servers
- 0
- Hooks
- 0
What it needs & plugs into
- API keys
- none
- Paid services
- none detected
- External tools
- none
- Talks to
- nothing external detected
Analyzed . Facts extracted from the plugin's files. Prose generated by claude-haiku-4-5-20251001.
Is this your plugin?
Claim it to keep the card accurate and enter the weekly contest. Requires signing in as the GitHub owner (trailofbits).