Vibe Index
🎯

lean4-theorem-proving

🎯Skill

from cameronfreer/lean4-skills

VibeIndex|
What it does

Provides core Lean 4 theorem proving workflows with 8 commands for automated proof generation, repair, analysis, and refinement using language server integration.

lean4-theorem-proving

Installation

Install skill:
npx skills add https://github.com/cameronfreer/lean4-skills --skill lean4-theorem-proving
2
AddedJan 25, 2026
View on GitHubBack to Skills

Skill Details

SKILL.md

Overview

# Lean 4 Skills for Claude

[![Run in Smithery](https://smithery.ai/badge/skills/cameronfreer)](https://smithery.ai/skills?ns=cameronfreer&utm_source=github&utm_medium=badge)

Claude Skills, commands, and agents for systematic development of formal proofs in Lean 4.

Plugins

| Plugin | Provides | Description |

|--------|----------|-------------|

| [lean4-theorem-proving](plugins/lean4-theorem-proving/) | Skill + 8 Commands | Core workflows, LSP integration, automation tools |

| [lean4-memories](plugins/lean4-memories/) | Skill | Persistent learning across sessions (requires MCP memory server) |

| [lean4-subagents](plugins/lean4-subagents/) | 5 Agents | Proof repair, sorry filling, axiom elimination, proof golfing |

Quick Start

```bash

# Via Marketplace (Recommended)

/plugin marketplace add cameronfreer/lean4-skills

/plugin install lean4-theorem-proving # Core (required)

/plugin install lean4-subagents # Optional: specialized agents

/plugin install lean4-memories # Optional: persistent memory

```

Skills activate automatically when you work on Lean 4 files. Commands appear in autocomplete with /lean4-theorem-proving: prefix.

What You Get

  • Lean LSP integration - Sub-second feedback vs 30s builds
  • 8 commands - /build-lean, /fill-sorry, /repair-file, /golf-proofs, /check-axioms, /analyze-sorries, /refactor-have, /search-mathlib
  • 5 specialized agents - Proof repair, sorry filling (fast + deep), axiom elimination, proof golfing
  • Automation scripts - 16 tools for search, analysis, verification
  • mathlib patterns - Type class management, domain-specific tactics

Highly recommended add-on: install the Lean LSP MCP Server alongside these plugins

The [lean-lsp-mcp](https://github.com/oOo0oOo/lean-lsp-mcp) server provides 12+ tools for rapid feedback, goal inspection, parallel tactic testing, and integrated lemma search. This dramatic speedup turns frustrating trial-and-error into smooth, interactive problem-solving. Our Lean 4 skill adds comprehensive workflow guides that teach the LLM to use the LSP tools effectively.

Setup: [INSTALLATION.md](INSTALLATION.md#lean-lsp-server) (<1 minute)

Documentation

  • [lean4-theorem-proving/README.md](plugins/lean4-theorem-proving/README.md) - Core skill guide
  • [lean4-subagents/README.md](plugins/lean4-subagents/README.md) - Specialized agents
  • [lean4-memories/README.md](plugins/lean4-memories/README.md) - Memory integration
  • [INSTALLATION.md](INSTALLATION.md) - Platform-specific setup, LSP server

Changelog

v3.4.2 (January 2026)

  • Updated lean-lsp-mcp documentation for v0.16-v0.19 features:

- New lean_profile_proof tool for identifying slow tactics

- Structured diagnostics output with success and failed_dependencies

- Expanded local Loogle setup instructions

  • Added lake build | tee tip to avoid redundant builds

v3.4.1 (January 2026)

  • Expanded /refactor-have to support both inlining and extraction
  • Added mathlib style guidance for idiomatic proofs

v3.4.0 (January 2026)

  • Added /refactor-have command for extracting long have-blocks
  • Added /repair-interactive command for interactive proof repair
  • Added lean4-sorry-filler-deep agent for complex sorries
  • Improved LSP integration and error handling

v3.3.0 (December 2025)

  • Added /repair-file command for full-file compiler-guided repair
  • Streamlined agent descriptions per Anthropic best practices

v3.2.0 (November 2025)

  • Enhanced mathlib search capabilities
  • Improved type class instance resolution patterns

v3.1.0 (October 2025)

  • Restructured as Claude Code marketplace with 3 plugins

Contributing

Contributions welcome! Open an issue or PR at https://github.com/cameronfreer/lean4-skills

License

MIT License - see [LICENSE](LICENSE)

More from this repository2

🏪
cameronfreer-lean4-skills🏪Marketplace

Enables Claude to systematically develop, analyze, and automate formal mathematical proofs in Lean 4 through integrated theorem proving commands, specialized agents, and workflow tools.

🎯
lean4-memories🎯Skill

Enables persistent learning and memory retention for Lean 4 theorem proving across different coding sessions by leveraging a memory server.