Claude Skill
cameronfreer/lean4-skills
Claude Skill for Lean 4 theorem proving. Configure AI-assisted formal verification, automate proof steps, and enhance mathematical reasoning workflows with this repository.
Overview
Repository
Install this Skill
git clone --depth 1 https://github.com/cameronfreer/lean4-skills.gitRegistry
git clone --depth 1 https://github.com/cameronfreer/lean4-skills.gitclaude mcp add --transport stdio --scope user lean-lsp -- uvx lean-lsp-mcpclaude mcp add --transport stdio --scope project lean-lsp -- uvx lean-lsp-mcp
Summary
A Claude Skill repository providing tools and configurations for Lean 4 theorem proving, enabling AI-assisted formal verification and mathematical reasoning.
Claude Skill 用于 Lean 4 定理证明
Key features
- Claude Skill integration for Lean 4
- AI-assisted theorem proving setup
- Configuration for formal verification workflows
Use cases
- Automating Lean 4 proof steps with AI
- Learning formal verification with Claude assistance
- Enhancing mathematical reasoning workflows
README excerpt
# 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. ## 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 | | 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 | | doctor | Diagnostics and migration help | **Claude Code:** invoke as `/lean4:<name>`. **Other hosts:** follow the corresponding workflow in [SKILL.md](plugins/lean4/skills/lean4/SKILL.md). Typical session: `draft` (or `formalize` / `autoformalize`) → `prove` (or `autoprove`) → `review` → `refactor` → `golf` → `checkpoint` → `git push`. CLI-like inputs are validated by a host-agnostic parser (`plugins/lean4/lib/command_args/`) for the six parameter-heavy commands. The Claude Code adapter pre-validates `/lean4:*` prompts via a `UserPromptSubmit` hook; other hosts fall back to model-parsed startup. Commands must announce resolved inputs, reject invalid startup configs, and treat wall-clock budgets as best-effort rather than host-enforced timeouts. See
Topics
No topics yet.