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