domains / families / software-engineering / lean4-memories

lean4-memories

separate

This skill should be used when working on Lean 4 formalization projects to maintain persistent memory of successful proof patterns, failed approaches, project conventions, and user preferences across sessions using MCP memory server integration

When to use

• **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
• Starting a new session on an existing project
• Encountering a proof pattern similar to previous work
• Trying an approach that previously failed

When not to use

• General Lean 4 workflows (4-Phase approach)
• mathlib search and tactics reference
• Automation scripts
• General domain-specific knowledge (measure theory, probability)

Skill page

Source