lean4-memories
Lean 4 Memories
Overview
This skill enables persistent learning and knowledge accumulation across Lean 4 formalization sessions by leveraging MCP (Model Context Protocol) memory servers. It transforms stateless proof assistance into a learning system that remembers successful patterns, avoids known dead-ends, and adapts to project-specific conventions.
Core principle: Learn from each proof session and apply accumulated knowledge to accelerate future work.
When to Use This Skill
This skill applies when working on Lean 4 formalization projects, especially:
- Multi-session projects - Long-running formalizations spanning days/weeks/months
- Repeated proof patterns - Similar theorems requiring similar approaches
- Complex proofs - Theorems with multiple attempted approaches
- Team projects - Shared knowledge across multiple developers
- Learning workflows - Building up domain-specific proof expertise
More from cameronfreer/lean4-skills
lean4
Use when editing .lean files, debugging Lean 4 builds (type mismatch, sorry, failed to synthesize instance, axiom warnings, lake build errors), searching mathlib for lemmas, formalizing mathematics in Lean, or learning Lean 4 concepts. Also trigger when the user asks for help with Lean 4, mathlib, or lakefile. Do NOT trigger for Coq/Rocq, Agda, Isabelle, HOL4, Mizar, Idris, Megalodon, or other non-Lean theorem provers.
99lean4-theorem-proving
Use when working with Lean 4 (.lean files), writing mathematical proofs, seeing "failed to synthesize instance" errors, managing sorry/axiom elimination, or searching mathlib for lemmas - provides build-first workflow, haveI/letI patterns, compiler-guided repair, and LSP integration
11