Agent Plugins Marketplace
← All plugins

writing-lean-proofs

v0.1.1

Structured Lean 4 proof writing and library design following Mathlib conventions

Claude Code1 Skill

By Fredrik Dahlgren7.1k GitHub starsUpdated last week

Directory evidence

Runtimes
Claude Code
Parsed components
1 skill or MCP entry
Source updated
Sep 16, 2026
Manifest status
Canonical path parsed

The directory validates manifest shape and source location. It does not execute the plugin or provide a security endorsement. Review the indexing methodology →

Install writing-lean-proofs for Claude Code

Installs for the current user
claude plugin marketplace add IchenDEV/agent-plugin-mkt
claude plugin marketplace update agent-plugin-marketplace
claude plugin install writing-lean-proofs@agent-plugin-marketplace

Paste and run these commands in a terminal with Claude Code. They add and refresh the PluginsMP catalog, then install this plugin.

The installer fetches third-party code from the source repository shown on this page. This directory validates manifest structure and source location, but does not perform a security audit; review the manifest, components, and source before installing.

Get the source manually
git clone https://github.com/trailofbits/skills

Clone the source repository, then follow its setup instructions to add the plugin to a compatible client. The plugin root is plugins/writing-lean-proofs/.

Plugin files

plugins/writing-lean-proofs/
├── .claude-plugin/plugin.json
└── skills/writing-lean-proofs/SKILL.md

Included Skills1

writing-lean-proofsskills/writing-lean-proofs/SKILL.md

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.

Plugin manifests1

plugins/writing-lean-proofs/.claude-plugin/plugin.json
{
  "name": "writing-lean-proofs",
  "version": "0.1.1",
  "description": "Structured Lean 4 proof writing and library design following Mathlib conventions",
  "author": {
    "name": "Fredrik Dahlgren",
    "email": "[email protected]",
    "url": "https://github.com/trailofbits"
  },
  "interface": {
    "displayName": "Writing Lean Proofs",
    "shortDescription": "Structured Lean 4 proof writing and library design following Mathlib conventions",
    "longDescription": "Structured Lean 4 proof writing and library design following Mathlib conventions",
    "developerName": "Fredrik Dahlgren"
  }
}

For maintainers

If you maintain this plugin, link to this source-backed listing from your README so users can review its manifest and indexed components.

[writing-lean-proofs on Agent Plugins Marketplace](https://pluginsmp.com/plugins/writing-lean-proofs)