Agent Plugins Marketplace
← All plugins

scaffold-lean-library

v1.0.2

Scaffold a Lean 4 library project with Mathlib or PFR dependencies, Lake test/lint wiring, GitHub Actions CI, text linting, and agent instructions.

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 scaffold-lean-library 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 scaffold-lean-library-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/scaffold-lean-library/.

Plugin files

plugins/scaffold-lean-library/
├── .claude-plugin/plugin.json
└── skills/scaffold-lean-library/SKILL.md

Included Skills1

scaffold-lean-libraryskills/scaffold-lean-library/SKILL.md

Scaffold a Lean 4 library project with Mathlib or PFR dependencies, Lake test/lint wiring, GitHub Actions CI, text linting, and agent instructions. Use when the user says "scaffold a Lean library", "new Lean project", "new Mathlib project", "create a Lean formalization repo", "start a Mathlib-downstream library", or "create a PFR downstream formalization". For Lean proof, naming, or module edits inside an existing project, use write-lean-code instead. For compile-time test modules in an existing project, use write-lean-tests.

Plugin manifests1

plugins/scaffold-lean-library/.claude-plugin/plugin.json
{
  "author": {
    "name": "Christopher Boone"
  },
  "description": "Scaffold a Lean 4 library project with Mathlib or PFR dependencies, Lake test/lint wiring, GitHub Actions CI, text linting, and agent instructions.",
  "homepage": "https://github.com/cboone/agent-harness-plugins",
  "keywords": [
    "lake",
    "lean",
    "mathlib",
    "pfr",
    "scaffolding"
  ],
  "license": "MIT",
  "name": "scaffold-lean-library",
  "repository": "https://github.com/cboone/agent-harness-plugins",
  "skills": "./skills",
  "version": "1.0.2"
}

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.

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