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

**Especially important when:**
- Starting a new session on an existing project
- Encountering a proof pattern similar to previous work
- Trying an approach that previously failed
- Needing to recall project-specific conventions
- Building on successful proof strategies from earlier sessions

## How Memory Integration Works

### Memory Scoping

All memories are scoped by:
1. **Project path** - Prevents cross-project contamination
2. **Skill context** - Memories tagged with `lean4-memories`
3. **Entity type** - Structured by pattern type (ProofPattern, FailedApproach, etc.)

**Example scoping:**
```
Project: /Users/freer/work/exch-repos/exchangeability-cursor
Skill: lean4-memories
Entity: ProofPattern:condExp_unique_pattern
```

### Memory Types

**1. ProofPattern** - Successful proof strategies
```
Store when: Proof completes successfully after exploration
Retrieve when: Similar goal pattern detected
```

**2. FailedApproach** - Known dead-ends to avoid
```
Store when: Approach attempted but failed/looped/errored
Retrieve when: About to t