This repository provides a comprehensive suite of Lean 4 theorem proving workflows designed for AI coding agents. It addresses the need for structured, repeatable, and efficient interaction with formal mathematical systems, enabling agents to draft, prove, review, and optimize Lean 4 code. The primary benefit is empowering AI agents with advanced capabilities in formal verification and mathematical reasoning, streamlining the development of reliable mathematical libraries and proofs.

How It Works

The project offers a collection of host-agnostic workflows, including draft, formalize, autoformalize, prove, autoprove, review, refactor, and golf. These workflows leverage a shared cycle engine that follows a Plan → Work → Checkpoint → Review → Replan → Continue/Stop pattern. Each cycle involves mathlib search, tactic application, and validation, ensuring a robust proving process. The host-agnostic design allows these core skills to function consistently across various AI coding platforms, with differences primarily in invocation methods.

Quick Start & Requirements

For Claude Code users, installation involves /plugin marketplace add cameronfreer/lean4-skills and /plugin install lean4. Other hosts require cloning the repository and following specific setup instructions in INSTALLATION.md for agents like Codex, Gemini, and Cursor. An optional, highly recommended Lean LSP MCP Server (lean-lsp-mcp) is available for significantly faster mathlib search and sub-second feedback, integrating via claude mcp add commands.

Highlighted Details

• Host-Agnostic Workflows: Core Lean 4 skills operate consistently across multiple AI coding agents.
• Comprehensive Workflow Suite: Covers the full lifecycle from initial drafting to advanced proof optimization and diagnostics.
• MCP Server Integration: Dramatically improves development feedback loops with faster search and diagnostics.
• Input Validation: A host-agnostic parser validates complex command inputs for parameter-heavy commands.

Maintenance & Community

Contributions via issues and pull requests are welcomed on GitHub. An optional lean4-contribute plugin assists agents in drafting bug reports and feature requests directly from the editor. No explicit community channels like Discord or Slack are mentioned in the README.

Licensing & Compatibility

The project is MIT licensed, permitting broad use and modification. Citing the repository is appreciated but not mandated by the license. No specific restrictions for commercial use or closed-source linking are noted, aligning with typical MIT license permissions.

Limitations & Caveats

Wall-clock budgets for autonomous workflows are treated as best-effort and are not host-enforced timeouts. Some host integrations are documented but not CI-verified. Project-scoped MCP servers might not propagate correctly to plugin subagents in certain Claude Code versions.