Deep Analysis

Complete Lean 4 theorem proving skill set for Claude, including LSP integration, automation commands, and specialized agents

Highly Recommended

Core Features

Sub-second feedback replacing 30-second build wait times

Including /build-lean, /fill-sorry, /repair-file, /golf-proofs, /check-axioms and other core commands

Proof repair, sorry filling (fast + deep), axiom elimination, proof simplification agents

16 automated tools for search, analysis, and verification

Type class management and domain-specific tactics support

Technical Implementation

Architecture:Modular plugin architecture with three independent plugins: lean4-theorem-proving (core), lean4-memories (persistent memory), lean4-subagents (specialized agents)

Execution Flow:

Key Components:

Lean 4

LSP (Language Server Protocol)

MCP Memory Server

Mathlib

Highlights

Sub-second LSP feedback greatly improves development efficiency
Complete command set covers entire proof development workflow
Specialized agents auto-handle complex proof tasks
Cross-session memory support for continuous learning of user habits
Actively maintained, still updated in January 2026

Use Cases

Lean 4 theorem proving development and debugging
Auto-filling sorry placeholders in proofs
Eliminating axiom dependencies in proofs
Optimizing and simplifying verbose proofs (proof golfing)
Searching mathlib for relevant theorems and tactics

Limitations

lean4-memories plugin requires MCP memory server configuration
Primarily for Lean 4, doesn't support Lean 3 or other proof assistants

Tech Stack

Lean 4Shell 脚本LSPMCP 协议Claude Code 插件系统

README

View on GitHub

Lean 4 Skills for Claude

Name: lean4-skills
Rating: 3.9 (8 reviews)
Author: cameronfreer

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

Plugins

Plugin	Provides	Description
lean4-theorem-proving	Skill + 8 Commands	Core workflows, LSP integration, automation tools
lean4-memories	Skill	Persistent learning across sessions (requires MCP memory server)
lean4-subagents	5 Agents	Proof repair, sorry filling, axiom elimination, proof golfing

Quick Start

# 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

Documentation

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

Changelog

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

🔍Deep Analysis