Agent Plugins Marketplace
← All plugins

write-lean-code

v1.0.4

Lean 4 style guide and Mathlib conventions for naming, proofs, formatting, and metaprogramming.

Claude Code1 Skill

By Christopher BooneLicense: MIT2 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 write-lean-code 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 write-lean-code-2@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/cboone/agent-harness-plugins

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

Plugin files

plugins/write-lean-code/
├── .claude-plugin/plugin.json
└── skills/write-lean-code/SKILL.md

Included Skills1

write-lean-codeskills/write-lean-code/SKILL.md

Lean 4 style guide and Mathlib conventions. Use whenever Lean code is the subject of the work, not only when editing: (1) writing, editing, or reviewing .lean files, (2) reading Lean source to answer a user question about it, (3) planning, proposing, or naming lemmas, definitions, theorems, or tactics before implementation, (4) discussing Lean design decisions, refactors, API choices, or proof strategies, (5) summarizing proof status or reporting on formalization progress, (6) writing or editing Lean docstrings and comments, (7) formalizing mathematical proofs, (8) writing custom tactics or metaprograms. Applies to any touch on .lean files or the proofs/ directory, including reading and discussion, not just edits. Covers naming, formatting, proof style, Mathlib conventions, general functional programming, and metaprogramming.

Plugin manifests1

plugins/write-lean-code/.claude-plugin/plugin.json
{
  "author": {
    "name": "Christopher Boone"
  },
  "description": "Lean 4 style guide and Mathlib conventions for naming, proofs, formatting, and metaprogramming.",
  "homepage": "https://github.com/cboone/agent-harness-plugins",
  "keywords": [
    "formal-methods",
    "lean",
    "lean4",
    "mathlib",
    "style"
  ],
  "license": "MIT",
  "name": "write-lean-code",
  "repository": "https://github.com/cboone/agent-harness-plugins",
  "skills": "./skills",
  "version": "1.0.4"
}

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.

[write-lean-code on Agent Plugins Marketplace](https://pluginsmp.com/plugins/write-lean-code-2)