Plugin marketplace

lean4-skills

Lean 4 theorem proving with guided + autonomous proving, LSP-first workflows, guardrails, and contribution helpers

486 · cameronfreer/lean4-skills2 pluginsMITupdated 5 days ago

Add this marketplace

Then install any plugin below by name — each page has its exact command.

lean4

claudecodex

Unified Lean 4 plugin (draft, formalize, autoformalize, prove, autoprove, disprove, checkpoint, review, refactor, golf, learn, diagnose) — LSP-first, scripts fallback

1 skill · 12 commands · 4 agents · hooks

486

lean4-contribute

claude

Draft and submit bug reports, feature requests, and insights as GitHub issues. Commands may share Lean code snippets with GitHub — review every draft before confirming.

3 commands

486

README badge

Shows how many plugins this repo ships, and links here.

claude & codex plugins2 plugins