lean4-memories
🎯Skillfrom cameronfreer/lean4-skills
|Enables persistent learning and memory retention for Lean 4 theorem proving across different coding sessions by leveraging a memory server.
Installation
npx skills add https://github.com/cameronfreer/lean4-skills --skill lean4-memoriesSkill Details
Overview
# Lean 4 Skills for Claude
[](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 | teetip to avoid redundant builds
v3.4.1 (January 2026)
- Expanded
/refactor-haveto support both inlining and extraction - Added mathlib style guidance for idiomatic proofs
v3.4.0 (January 2026)
- Added
/refactor-havecommand for extracting long have-blocks - Added
/repair-interactivecommand for interactive proof repair - Added
lean4-sorry-filler-deepagent for complex sorries - Improved LSP integration and error handling
v3.3.0 (December 2025)
- Added
/repair-filecommand 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
Enables Claude to systematically develop, analyze, and automate formal mathematical proofs in Lean 4 through integrated theorem proving commands, specialized agents, and workflow tools.
Provides core Lean 4 theorem proving workflows with 8 commands for automated proof generation, repair, analysis, and refinement using language server integration.