# Lean 4 Skills: A Structured Proving Loop for AI Coding Agents > cameronfreer/lean4-skills packages a prove/review/golf workflow for AI agents working in Lean 4, with host-agnostic installation and a shared cycle engine. The core value is discipline: it forces agents to plan, checkpoint, and review instead of guessing at proofs. **cameronfreer/lean4-skills** — Lean 4 theorem proving skill and workflow pack for AI coding agents - Repository: https://github.com/cameronfreer/lean4-skills - Stars: 469 · Forks: 46 - Language: Shell - License: MIT - Published: 2026-08-21 · Updated: 2026-08-21 · Language: en - Canonical page: https://hysenlabs.com/projects/cameronfreer-lean4-skills ## What This Pack Actually Solves AI coding agents are good at producing plausible Lean 4 code, but they are equally good at producing proofs that do not compile or that rely on forbidden axioms. This repository addresses that by turning theorem proving into a structured workflow: draft, formalize, prove, review, refactor, golf, checkpoint. It is aimed at engineers who use Claude Code, Codex, Gemini CLI, Cursor, or similar tools and want the agent to follow a repeatable loop rather than improvise. The README frames it as a 'workflow pack', not a tactic library. There is no new automation for finding proofs; instead, the pack constrains how the agent works: when to search mathlib, when to stop, and when to force a review. That distinction matters because most Lean tooling focuses on the prover itself, not on the process around it. ## The Shared Proof Cycle: Plan, Work, Checkpoint, Review, Replan The proving workflows (prove, autoprove, formalize, autoformalize) all share one cycle: Plan, Work, Checkpoint, Review, Replan, Continue/Stop. Each `sorry` triggers a mathlib search, tactic attempts, and validation. If the agent gets stuck, the cycle forces a review and a replan. This is a deliberate design choice: it prevents the agent from burning tokens on endless tactic guessing. The README notes that `prove` and `autoprove` keep declaration headers immutable, while `formalize` and `autoformalize` allow statement changes. That separation is practical because changing a theorem statement during a proof attempt can hide the original problem. The checkpoint step is not just a save; it includes a project build, an axiom check, and a commit. So the cycle bakes in verification at every stage, not just at the end. The 'autoprove' variant adds explicit stop budgets, which is a concrete mechanism for controlling cost and time. ## Installation Tiers: From Native Plugins to a Portable Checkout Installation is tiered by host. Claude Code gets a native plugin with `/lean4:*` commands, hooks, guardrails, subagents, and a helper runtime. Codex gets a native plugin with trusted hooks and an absolute-path helper runtime, but without `/lean4:*` parity. Other hosts like Gemini, Antigravity, Copilot, Cursor, Windsurf, and OpenCode get a 'skill-only' install: instructions and references, documented but not CI-verified. For any host, there is a portable checkout (Tier 2) that includes skill, wrappers, and helper scripts. The README is explicit that host-native installers generally provide only instructions and references; you need the portable runtime if you want the bundled wrappers. For Claude Code, the commands are `/plugin marketplace add cameronfreer/lean4-skills` and `/plugin install lean4`. For Codex, it is `codex plugin marketplace add cameronfreer/lean4-skills --ref main` and `codex plugin add lean4@lean4-skills`. This tiering is honest about where support is solid and where it is aspirational. ## The Command Invocation Contract and Host-Agnostic Parsing Seven parameter-heavy commands use a host-agnostic parser to validate CLI-like inputs. This is a significant architectural decision. Instead of writing separate command handlers for each host, the pack defines a contract that any host can invoke. The parser validates arguments before the workflow starts, which catches malformed input early. The README points to a reference file, `command-invocation.md`, for details. This contract is what allows the same core skill to work across Claude Code, Codex, and others. But it also means that hosts without native plugin support may not expose the full command surface. The README's table shows Codex lacks `/lean4:*` parity, so you should expect differences in how commands are invoked. For a team standardizing on one host, this is fine. For a team mixing hosts, the contract reduces, but does not eliminate, the need to learn host-specific quirks. ## Verification and CI: What Is Actually Tested The repository's CI gates every PR with full documentation lint, semantic contract suites, and hook and wrapper runtime tests on Linux and macOS Bash 3.2. It also pins shellcheck, ruff, mypy, and actionlint. This is a strong signal for a project that is mostly shell scripts and documentation. The README is careful to say that hosts marked 'documented' in the Quick Start table follow verified setup patterns but are not CI-tested. So Claude Code and Codex are the only hosts with verified full-plugin installations. This matters if you plan to use Cursor or Windsurf: the setup may work, but the project does not claim it is tested. The CI also runs semantic contract suites, which suggests the workflows have testable behavior beyond just 'runs without error'. That is rare in this kind of tooling and worth checking if you adopt it. ## Limitations and When It Is the Wrong Tool The most obvious limitation is that the pack does not improve your agent's actual proving ability. It imposes structure, but if the underlying model cannot find a proof, the cycle will just loop through review and replan until it hits the stop budget. For a hard theorem, that means wasted tokens. The README also notes that editing `.lean` files without a command runs only 'one bounded pass', which is a guardrail but also a restriction: you cannot rely on the agent to make broad, unplanned changes. Another limitation is host support. The README explicitly marks non-Claude/Codex hosts as 'documented, not CI-verified'. If you are on a less common host, you are the test suite. Finally, the pack is tightly coupled to Lean 4 and mathlib. It is useless for other proof assistants like Coq or Isabelle. If your project is not in Lean 4, this is not the tool. ## Alternatives: Lean LSP MCP and Raw Agent Prompts The README itself recommends pairing this pack with lean-lsp-mcp, a separate project that provides live goal inspection and mathlib search. That is not a direct alternative; it is a complement. The real alternative is to skip the pack entirely and write your own agent prompts or use a plain Lean 4 language server. The difference is approach: lean-lsp-mcp gives the agent better real-time feedback, so it can make more informed tactic choices, but it does not enforce a workflow. This pack enforces the workflow but relies on the agent's existing ability to use tactics. If your agent is already competent at Lean, the pack adds discipline and safety checks. If your agent is weak, no workflow will save it. Another alternative is to use Lean's own `#check` and `#eval` commands interactively, but that is manual and does not scale to multi-file projects. The pack's checkpoint and axiom-check features are what you lose by going raw. ## Maintenance, Licensing, and Upgrade Path The repository is MIT licensed, which is permissive and suitable for commercial use. The README includes a CITATION.cff and a BibTeX entry, but citation is not required by the license. There is a CHANGELOG.md and a MIGRATION.md for moving from v3 to v4, which suggests the project takes upgrade pain seriously. Recent releases are frequent: v4.7.0, v4.6.9, and v4.6.8 within a week. That is a double-edged sword. Frequent releases mean active maintenance, but they also mean you should pin a version if you rely on stable behavior. The MIGRATION.md is specifically for Claude Code users, so other hosts may have less guidance. The `lean4-contribute` plugin is an opt-in helper that lets your agent draft bug reports or feature requests. It only drafts after you opt in and shows every draft before sending. That is a thoughtful privacy measure, but it is an extra component to manage. Overall, maintenance cost is moderate: you need to track releases, test on your host, and re-verify the portable runtime after updates. ## Conclusion Adopt this if your AI agent regularly edits Lean 4 files and you want a bounded, repeatable proving loop with explicit stop budgets and axiom checks. Skip it if you only need one-off tactic suggestions or if your host lacks native plugin support and you dislike managing a portable runtime. Before adopting, verify the command invocation contract against your host's plugin capabilities, and test the portable checkout on your CI image, since only Claude Code and Codex are CI-tested. The repository is MIT licensed and actively released, but the documentation explicitly marks non-Claude/Codex hosts as 'documented, not CI-verified', so treat those setups as best-effort until you run them yourself. ## FAQ ### What does cameronfreer/lean4-skills do? It is a workflow pack for AI coding agents doing Lean 4 theorem proving, giving them a shared prove, review and golf loop plus mathlib search, axiom checking and safety guardrails. There are twelve workflows, from draft and formalize through prove, autoprove, disprove, review, refactor, golf, checkpoint, learn and diagnose. ### How do I install lean4-skills in Claude Code? Run `/plugin marketplace add cameronfreer/lean4-skills` and then `/plugin install lean4` in chat. That is the Tier 3 native plugin, which gives you the skill, `/lean4:*` commands, hooks, guardrails, subagents and the helper runtime. Codex uses a marketplace add plus a plugin add from its shell instead. ### Which agent hosts are actually tested for lean4-skills? Only Claude Code and Codex. Every other Agent Skills host, including Gemini CLI, Copilot, Cursor, Windsurf and OpenCode, gets a skill-only quick install that is documented but not CI-verified. CI itself runs documentation lint, semantic contract suites and hook and wrapper runtime tests on Linux and macOS Bash 3.2. ### What is the difference between prove and autoprove in lean4-skills? Both share the same Plan, Work, Checkpoint, Review, Replan cycle and both keep declaration headers immutable. The difference is agency and budget: prove is guided cycle by cycle with you in the loop, while autoprove is autonomous across multiple cycles and carries explicit stop budgets. ### Do I need the Lean LSP MCP server to use lean4-skills? No, the skill works standalone. The pack recommends pairing with lean-lsp-mcp because live goal inspection and mathlib search typically give much faster feedback than repeated full builds. Registration is documented for any host, with a scope trade-off specific to Claude Code if you use subagents. ## Sources - [Official README](https://github.com/cameronfreer/lean4-skills#readme) - [Project repository](https://github.com/cameronfreer/lean4-skills) - [Release notes](https://github.com/cameronfreer/lean4-skills/releases) --- Hysen Labs editorial analysis, written from the project's own repository and release notes. Cite the canonical page: https://hysenlabs.com/projects/cameronfreer-lean4-skills