AI & Agents
Plugin
lean4-skills
Lean 4 workflow pack for AI coding agents. Gives your agent a structured prove/review/golf loop, mathlib search, axiom checking, and safety guardrails.
Plugin Signal76/100Solid
maintained99
capable62
documented75
adopted54
Install on Claude Code
> /plugin marketplace add cameronfreer/lean4-skills
What's inside
Agent(4 agents)
axiom-eliminatorRemove nonconstructive axioms by refactoring proofs to structure (kernels, measurability, etc.). Use after checking axiom hygiene to systematically eliminate custom axioms.proof-golferGolf 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-repairCompiler-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-deepStrategic resolution of stubborn sorries; may refactor across files within the header fence. Use when fast pass fails or for complex proofs.
Command(14 commands)
/bug-reportDraft a bug report issue for lean4-skills/feature-requestDraft a feature request issue for lean4-skills/share-insightDraft a shareable insight from your session as a GitHub issue/autoformalizeAutonomous end-to-end formalization from informal sources/autoproveAutonomous multi-cycle theorem proving with explicit stop budgets/checkpointSave progress with a safe commit checkpoint
README
Lean 4 Skills
Lean 4 workflow pack for AI coding agents. Gives your agent a structured prove/review/golf loop, mathlib search, axiom checking, and safety guardrails. The workflows are host-agnostic — Claude Code, Codex, Gemini CLI, Cursor, and others all use the same core skill; only the invocation surface differs.
Quick Start
| Host | Recommended installation | What you get | Details |
|---|---|---|---|
| Claude Code | Native plugin (Tier 3) | Skill + /lean4:* commands, hooks, guardrails, subagents, helper runtime | Claude Code |
| Codex | Native plugin (Tier 3) | Skill + trusted hooks + absolute-path helper runtime; no /lean4:* parity | Codex |
| Other Agent Skills hosts (Gemini, Antigravity, Copilot, Cursor, Windsurf, OpenCode, …) | Skill-only quick install | Instructions + references (documented, not CI-verified) | Installation guide |
| Any host, full runtime | Portable checkout (Tier 2) | Skill + wrappers + helper scripts | Portable |
Claude Code (run in chat):
/plugin marketplace add cameronfreer/lean4-skills
/plugin install lean4
Codex (in your shell):
codex plugin marketplace add cameronfreer/lean4-skills --ref main
codex plugin add lean4@lean4-skills
Host-native skill installers generally provide the instructions and references only. Use the portable runtime when you also need the bundled wrappers and scripts; Claude Code and Codex provide native full-plugin installations.
Workflows
| Workflow | Description |
|---|---|
| draft | Draft Lean declaration skeletons from informal claims |
| formalize | Interactive formalization — drafting plus guided proving |
| autoformalize | Autonomous end-to-end formalization from informal sources |
| prove | Guided cycle-by-cycle theorem proving |
| autoprove | Autonomous multi-cycle proving with explicit stop budgets |
| disprove | Guided counterexample search with certified refutation |
| checkpoint | Save point (per-file + project build, axiom check, commit) |
| review | Read-only quality review |
| refactor | Leverage mathlib, extract helpers, simplify proof strategies |
| golf | Improve proofs for directness, clarity, performance, and brevity |
| learn | Interactive teaching and mathlib exploration |
| diagnose | Diagnostics and migration help |
Claude Code: invoke as /lean4:<name>. Other hosts: follow the corresponding workflow in SKILL.md.
Typical session: draft (or formalize / autoformalize) → prove (or autoprove) → review → refactor → golf → checkpoint → git push. Use disprove instead of prove to refute a statement rather than prove it.
CLI-like inputs to the seven parameter-heavy commands are validated by a host-agnostic parser — see the Command Invocation Contract.
The Shared Proof Cycle
The proving workflows (prove, autoprove, formalize, and autoformalize) share one cycle — Plan → Work → Checkpoint → Review → Replan → Continue/Stop — where each sorry gets a mathlib search, tactic attempts, and validation, and being stuck forces a review + replan. Statement and header changes belong to the synthesis workflows (formalize / autoformalize); prove and autoprove keep declaration headers immutable. Editing .lean files without a command runs one bounded pass — fix the immediate issue, then hand off to the right workflow — with the Blocked-Goal Triage loop for a goal that resists it. Details: cycle-engine.md.
Verification
CI gates every PR: full documentation lint, semantic contract suites, hook and wrapper runtime tests on Linux and macOS Bash 3.2, and pinned shellcheck/ruff/mypy/actionlint. Hosts marked "documented" in the Quick Start table follow verified setup patterns but are not CI-tested.
Lean LSP MCP (Optional, Recommended)
The skill works standalone, but pairs best with lean-lsp-mcp: live goal inspection, mathlib search, and typically much faster feedback than repeated full builds. See INSTALLATION.md → MCP Server for registration on any host, including the Claude Code scope trade-off for subagent visibility.
Documentation
- INSTALLATION.md — installation tiers, host sections, MCP setup
- SKILL.md — core skill reference
- Commands — command documentation
- References — cycle engine, mathlib style, proof golfing, tactic patterns, grind, metaprogramming, and more
- lean4-contribute — opt-in helper for filing bug reports, feature requests, and insights from your editor
- CHANGELOG.md — version history
- MIGRATION.md — migrating from v3 (Claude Code)
Contributing
Issues and PRs welcome at https://github.com/cameronfreer/lean4-skills. With the lean4-contribute plugin installed, your agent may suggest filing bug reports, feature requests, or insights at natural stopping points — drafting starts only after you opt in, and every draft is shown in full before anything is sent.
License & Citation
MIT licensed. See LICENSE for more information.
Citing this repository is highly appreciated but not required by the license. See also CITATION.cff.
@software{lean4-skills,
author = {Cameron Freer},
title = {Lean 4 {Skills}: Theorem proving skill and workflow pack for {AI} coding agents},
url = {https://github.com/cameronfreer/lean4-skills},
month = oct,
year = {2025}
}
File tree
cameronfreer/lean4-skillsView on GitHub
.agents/
plugins/
marketplace.json
.claude-plugin/
marketplace.json
.github/
workflows/
bash3-compat.yml
lint.yml
release.yml
.gitignore
CHANGELOG.md
CITATION.cff
INSTALLATION.md
LICENSE
plugins/
lean4/
lean4-contribute/
.claude-plugin/
plugin.json
commands/
bug-report.md
feature-request.md
share-insight.md
README.md
tools/
lint_contribute.sh
.claude-plugin/
plugin.json
.codex-plugin/
plugin.json
agents/
axiom-eliminator.md
proof-golfer.md
proof-repair.md
sorry-filler-deep.md
bin/
lean4-skills-analyze-let-usage
lean4-skills-check-axioms-inline
lean4-skills-cycle-tracker
lean4-skills-disprove-artifact-txn
lean4-skills-disprove-emit-artifact
lean4-skills-disprove-method-probe
lean4-skills-disprove-target-profile
lean4-skills-disprove-target-resolve
lean4-skills-file-baseline
lean4-skills-find-exact-candidates
lean4-skills-find-golfable
lean4-skills-find-usages
lean4-skills-preflight
lean4-skills-project-context
lean4-skills-search-mathlib
lean4-skills-smart-search
lean4-skills-sorry-analyzer
commands/
autoformalize.md
autoprove.md
checkpoint.md
diagnose.md
disprove.md
draft.md
formalize.md
golf.md
learn.md
prove.md
refactor.md
review.md
GUARDRAILS.md
hooks/
bootstrap.sh
codex-hooks.json
guardrails.sh
hooks.json
validate_user_prompt.py
lib/
command_args/
__init__.py
coercions.py
formatter.py
parser.py
specs/
__init__.py
_common.py
autoformalize.py
autoprove.py
disprove.py
draft.py
formalize.py
learn.py
prove.py
target_patterns.py
tokenizer.py
types.py
data/
disprove_methods.toml
disprove_methods.py
scripts/
analyze_let_usage.py
check_axioms_inline.sh
cycle_tracker.sh
disprove_artifact_txn.py
disprove_emit_artifact.py
disprove_method_probe.py
disprove_target_profile.py
disprove_target_resolve.py
file_baseline.py
find_exact_candidates.py
find_golfable.py
find_instances.sh
find_usages.sh
minimize_imports.py
parse_command_args.py
parse_lean_errors.py
preflight_env.sh
project_context.py
README.md
search_mathlib.sh
smart_search.sh
solver_cascade.py
sorry_analyzer.py
test_apply_exact_chains.py
TESTING.md
tests/
test_file_baseline.py
test_ordering.py
test_project_context.py
test_sorry_analyzer.py
try_exact_at_step.py
unused_declarations.sh
MIGRATION.md
README.md
scripts
skills/
lean4/
agents/
openai.yaml
references/
agent-workflows.md
axiom-elimination.md
calc-patterns.md
command-examples.md
command-invocation.md
compilation-errors.md
compiler-guided-repair.md
compiler-internals.md
cycle-engine.md
disprove-engine.md
domain-patterns.md
ffi-interop.md
grind-tactic.md
instance-pollution.md
json-patterns.md
lean-lsp-server.md
lean-lsp-tools-api.md
lean-phrasebook.md
lean4-custom-syntax.md
learn-pathways.md
linter-authoring.md
mathlib-guide.md
mathlib-style.md
measure-theory.md
metaprogramming-patterns.md
performance-optimization.md
profiling-workflows.md
project-context.md
proof-golfing-patterns.md
proof-golfing.md
proof-refactoring.md
proof-simplification.md
proof-templates.md
review-hook-schema.md
scaffold-dsl.md
simp-reference.md
sorry-filling.md
subagent-workflows.md
tactic-patterns.md
tactics-reference.md
verso-docs.md
SKILL.md
tests/
command_args/
__init__.py
_doc_sync_allowlist.py
_doc_sync_forward_exclusions.py
test_formatter.py
test_hook_block_roundtrip.py
test_parse_command_args_cli.py
test_parser_autoformalize.py
test_parser_autoprove.py
test_parser_common.py
test_parser_disprove.py
test_parser_draft.py
test_parser_formalize.py
test_parser_learn.py
test_parser_prove.py
fixtures/
axiom_check/
axiom_decl.lean
bare_end.lean
bin/
lake
custom_axiom.lean
dotted_namespace.lean
imports_only.lean
indented_decl.lean
legacy_format.lean
modifier_decls.lean
multi_sibling_namespace.lean
named_section_inside_namespace.lean
nested_namespace.lean
no_axioms.lean
primed_name.lean
private_decl.lean
same_file_custom_and_unknown.lean
same_file_partial.lean
section_inside_namespace.lean
silent_parser_miss.lean
single_namespace.lean
standard_substring.lean
unqualified.lean
wrong_name.lean
zero_coverage.lean
unused_decls/
all_used/
Sample.lean
expanded_classes/
Sample.lean
has_unused/
Sample.lean
imports_only/
Sample.lean
indented_modifier/
Sample.lean
mixed_dir/
Dead.lean
Used.lean
private_only/
Sample.lean
pressure/
disprove_prime_directive.md
test_bash3_smoke.sh
test_bootstrap_env.sh
test_check_axioms_inline.sh
test_codex_adapter.sh
test_cycle_tracker.sh
test_disprove_artifact_txn.sh
test_disprove_emit_artifact.sh
test_disprove_flow.sh
test_disprove_method_probe.py
test_disprove_methods.py
test_disprove_target_profile.sh
test_disprove_target_resolve.sh
test_guardrails.sh
test_lint_docs.sh
test_lint_runtime_portability.sh
test_preflight_env.sh
test_release_notes.sh
test_unused_declarations.sh
test_validate_user_prompt.sh
test_wrapper_runtime.sh
tools/
lint_docs.sh
lint_runtime_portability.sh
release_notes.sh
smoke_snippets.sh
test_contracts.sh
pyproject.toml
README.md
TESTING.mdFAQ
lean4-skills is a Claude Code plugin with 1 hand-picked skill for ai & agents work, indexed on Flowy. Install it with the command on its page. It includes lean4. Its skills do not fire on their own yet. Request auto-invocation to have Flowy route them as you prompt. Free and open source.
- What is lean4-skills?
- Lean 4 workflow pack for AI coding agents. Gives your agent a structured prove/review/golf loop, mathlib search, axiom checking, and safety guardrails.
- How do I install lean4-skills?
- Run these in Claude Code: /plugin marketplace add cameronfreer/lean4-skills. Then prompt normally.
- Does lean4-skills auto-invoke its skills?
- Not yet. It is indexed on Flowy as a plain plugin. Request auto-invocation on its page and Flowy will route its skills for you as you prompt.
- Is lean4-skills free?
- Yes. Flowy is free and open source, with nothing gated. You can read every skill in full before you install.