claudecodex

lean4

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

486 on GitHubby Cameron Freerv4.12.0MITupdated 5 days agoCoding
/

Plugin lean4 from marketplace lean4-skills in cameronfreer/lean4-skills. Commands read from the repo's manifest — 5 days ago.

This plugin runs code on your machine — its hooks fire automatically on events like tool use. The exact commands are listed below; read them before installing.

What it installs

Skills (1)

  • lean4

    Use when editing .lean files, debugging Lean 4 builds (type mismatch, sorry, failed to synthesize instance, axiom warnings, lake build errors), searching mathlib for lemmas, formalizing mathematics in Lean, finding a counterexample to, refuting, or disproving a Lean statement, or learning Lean 4 con

Slash commands (12)

  • /lean4:autoformalize

    Autonomous end-to-end formalization from informal sources

  • /lean4:autoprove

    Autonomous multi-cycle theorem proving with explicit stop budgets

  • /lean4:checkpoint

    Save progress with a safe commit checkpoint

  • /lean4:diagnose

    Diagnostics, cleanup, and migration help

  • /lean4:disprove

    Guided counterexample search with certified refutation

  • /lean4:draft

    Draft Lean declaration skeletons from informal claims

  • /lean4:formalize

    Interactive formalization — drafting plus guided proving

  • /lean4:golf

    Improve Lean proofs for directness, clarity, performance, and brevity

  • /lean4:learn

    Interactive teaching and mathlib exploration

  • /lean4:prove

    Guided cycle-by-cycle theorem proving with explicit checkpoints

  • /lean4:refactor

    Leverage mathlib, extract helpers, simplify proof strategies

  • /lean4:review

    Read-only code review of Lean proofs

Subagents (4)

  • axiom-eliminator

    Remove nonconstructive axioms by refactoring proofs to structure (kernels, measurability, etc.). Use after checking axiom hygiene to systematically eliminate custom axioms.

  • proof-golfer

    Golf Lean 4 proofs after they compile; improve proofs for directness, clarity, performance, and brevity without changing semantics. Use after successful compilation to achieve 30-40% size reduction.

  • proof-repair

    Compiler-guided iterative proof repair with two-stage repair escalation (fast → strong). Use for error-driven proof fixing with small sampling budgets (K=1).

  • sorry-filler-deep

    Strategic resolution of stubborn sorries; may refactor across files within the header fence. Use when fast pass fails or for complex proofs.

Hooks (3)

  • SessionStart

    ${CLAUDE_PLUGIN_ROOT}/hooks/bootstrap.sh

  • UserPromptSubmit

    ${CLAUDE_PLUGIN_ROOT}/hooks/validate_user_prompt.py

  • PreToolUse

    ${CLAUDE_PLUGIN_ROOT}/hooks/guardrails.sh

View source on GitHub

More from cameronfreer/lean4-skills

All 2 plugins →

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

Similar plugins

mattpocock-skills

claude

Matt Pocock's agent skills for real engineering (grilling, spec/ticket flows, TDD, code review, domain modelling and more).

39 skills

mattpocock/skills 323,108

superpowers

claudecodex

Core skills library for Claude Code: TDD, debugging, collaboration patterns, and proven techniques

15 skills · hooks

obra/superpowers 316,836

claude-mem

claudecodex

Persistent memory for Claude Code: the next session starts where the last one left off.

29 skills · 1 MCP server · hooks

thedotmack/claude-mem 116,618

career-ops

claudecodex

Open-source AI job search that runs locally in your AI coding CLI: scan job portals, evaluate listings into a structured A-H report with a 1-5 score, tailor your CV, track applications

5 skills · hooks

career-ops-hq/career-ops 82,253

mem0

claudecodex

Cross-session memory and token savings for coding agents.

6 skills · 1 agent · 1 MCP server · hooks

mem0ai/mem0 68,893

context7

claudecodex

Up-to-date documentation lookup. Pull version-specific documentation and code examples directly from source repositories into your coding agent's context.

1 MCP server

upstash/context7 64,709

Maintain lean4?

This page updates itself from your repo. Add the badge to your README, or get it Featured to pin it above the organic results with a followed link to your site.

claude & codex plugins2 plugins