lean4-memories

by benchflow-ai

Install this Skill

curl -fsSL -o lean4-memories.zip https://skill.seembox.com/api/v1/skills/lean4-memories/download && unzip lean4-memories.zip

Download lean4-memories.zip

SKILL.md About

---
name: lean4-memories
description: 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
---

# 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 try similar approach
```

**3. ProjectConvention** - Code style and patterns
```
Store when: Consistent pattern observed (naming, structure, tactics)
Retrieve when: Creating new definitions/theorems
```

**4. UserPreference** - Workflow customization
```
Store when: User expresses preference (verbose output, specific tools, etc.)
Retrieve when: Choosing between options
```

**5. TheoremDependency** - Relationships between theorems
```
Store when: One theorem proves useful for proving another
Retrieve when: Looking for helper lemmas
```

## Memory Workflows

### Storing Memories

**After successful proof:**
```lean
-- Just proved: exchangeable_iff_fullyExchangeable
-- Store the successful pattern
```

Store:
- Goal pattern: `exchangeable X ↔ fullyExchangeable X`
- Successful tactics: `[apply measure_eq_of_fin_marginals_eq, intro, simp]`
- Helper lemmas used: `[prefixCylinder_measurable, isPiSystem_prefixCylinders]`
- Difficulty: medium (54 lines)
- Confidence: high (proof clean, no warnings)

**After failed approach:**
```lean
-- Attempted: simp only [condExp_indicator, mul_comm]
-- Result: infinite loop, build timeout
```

Store:
- Failed tactic: `simp only [condExp_indicator, mul_comm]`
- Error: "infinite simp loop"
- Context: conditional expectation with indicator
- Recommendation: "Use simp only [condExp_indicator] without mul_comm"

**Project conventions observed:**
```lean
-- Pattern: All measure theory proofs start with haveI
haveI : MeasurableSpace Ω := inferInstance
```

Store:
- Convention: "Measure theory proofs require explicit MeasurableSpace instance"
- Pattern: `haveI : MeasurableSpace Ω`
- Frequency: 15 occurrences
- Files: DeFinetti/ViaL2.lean, Core.lean, Contractability.lean

### Retrieving Memories

**Starting new proof session:**
1. Load project-specific conventions
2. Retrieve similar proof patterns from past work
3. Surface any known issues with current file/module

**Encountering similar goal:**
```
⊢ condExp μ m X =ᵐ[μ] condExp μ m Y

Memory retrieved: "Similar goals proved using condExp_unique"
Pattern: "Show ae_eq, verify measurability, apply condExp_unique"
Success rate: 3/3 in this project
```

**Before trying a tactic:**
```
About to: simp only [condExp_indicator, mul_comm]

Memory retrieved: ⚠️ WARNING - This combination causes infinite loop
Failed in: ViaL2.lean:2830 (2025-10-17)
Alternative: Use simp only [condExp_indicator], then ring
```

## Integration with lean4-theorem-proving Skill

The lean4-memories skill complements (doesn't replace) lean4-theorem-proving:

**lean4-theorem-proving provides:**
- General Lean 4 workflows (4-Phase approach)
- mathlib search and tactics reference
- Automation scripts
- Domain-specific knowledge (measure theory, probability)

**lean4-memories adds:**
- Project-specific learned patterns
- History of what worked/failed in this project
- Accumulated domain expertise from your proofs
- Personalized workflow preferences

**Use together:**
1. lean4-theorem-proving guides general workflow
2. lean4-memories provides project-specific context
3. Memories inform tactics choices from lean4-theorem-proving

## Memory Operations

### Storing a Successful Proof Pattern

After completing a proof, store the pattern using MCP memory:

**What to capture:**
- **Goal pattern** - Type/structure of goal (equality, exists, forall, etc.)
- **Tactics sequence** - Tactics that worked, in order
- **Helper lemmas** - Key lemmas applied
- **Difficulty** - Lines of proof, complexity estimate
- **Confidence** - Clean proof vs sorries/warnings
- **Context** - File, module, theorem name

**When to store:**
- Proof completed successfully (no sorries)
- Non-trivial (>10 lines or required exploration)
- Likely to be useful again (similar theorems expected)

**Storage format:**
```
Entity type: ProofPattern
Name: {descriptive_name}
Attributes:
  - project: {absolute_path}
  - goal_pattern: {pattern_description}
  - tactics: [list, of, tactics]
  - helper_lemmas: [lemma1, lemma2]
  - difficulty: {small|medium|large}
  - confidence: {0.0-1.0}
  - file: {filename}
  - timestamp: {date}
```

### Storing a Failed Approach

When an approach fails (error, loop, timeout), store to avoid repeating:

**What to capture:**
- **Failed tactic** - Exact tactic/sequence that failed
- **Error type** - Loop, timeout, type error, etc.
- **Context** - What was being proved
- **Alternative** - What worked instead (if known)

**When to store:**
- Infinite simp loops
- Tactics causing build timeouts
- Type mismatches from subtle issues
- Approaches that seemed promising but didn't work

**Storage format:**
```
Entity type: FailedApproach
Name: {descriptive_name}
Attributes:
  - project: {absolute_path}
  - failed_tactic: {tactic_text}
  - error: {error_description}
  - context: {what_was_being_proved}
  - alternative: {what_worked}
  - timestamp: {date}
```

### Storing Project Conventions

Track consistent patterns that emerge:

**What to capture:**
- **Naming conventions** - h_ for hypotheses, have_ for results
- **Proof structure** - Standard opening moves (haveI, intro patterns)
- **Import patterns** - Commonly used imports
- **Tactic preferences** - measurability vs explicit proofs

**When to store:**
- Pattern observed 3+ times consistently
- Convention affects multiple files
- Style guide established

### Retrieving Memories

**Before starting proof:**
```
1. Query for similar goal patterns
2. Surface successful tactics for this pattern
3. Check for known issues with current context
4. Suggest helper lemmas from similar proofs
```

**During proof:**
```
1. Before each major tactic, check for known failures
2. When stuck, retrieve alternative approaches
3. Suggest next tactics based on past success
```

**Query patterns:**
```
# Find similar proofs
search_entities(
  query="condExp equality goal",
  filters={"project": current_project, "entity_type": "ProofPattern"}
)

# Check for failures
search_entities(
  query="simp only condExp_indicator",
  filters={"project": current_project, "entity_type": "FailedApproach"}
)

# Get conventions
search_entities(
  query="naming conventions measure theory",
  filters={"project": current_project, "entity_type": "ProjectConvention"}
)
```

## Best Practices

### Memory Quality

**DO store:**
- ✅ Successful non-trivial proofs (>10 lines)
- ✅ Failed approaches that wasted significant time
- ✅ Consistent patterns observed multiple times
- ✅ Project-specific insights

**DON'T store:**
- ❌ Trivial proofs (rfl, simp, exact)
- ❌ One-off tactics unlikely to recur
- ❌ General Lean knowledge (already in training/mathlib)
- ❌ Temporary workarounds

### Memory Hygiene

**Confidence scoring:**
- **High (0.8-1.0)** - Clean proof, no warnings, well-tested
- **Medium (0.5-0.8)** - Works but has minor issues
- **Low (0.0-0.5)** - Hacky solution, needs refinement

**Aging:**
- Recent memories (same session) = higher relevance
- Older memories = verify still applicable
- Patterns from many sessions = high confidence

**Pruning:**
- Remove memories for deleted theorems
- Update when better approach found
- Mark as outdated if project evolves

### User Control

**Users can:**
- Toggle lean4-memories skill on/off independently
- Clear project-specific memories
- Review stored memories
- Adjust confidence thresholds
- Export/import memories for sharing

## Example Workflow

**Session 1: First proof**
```lean
-- Proving: measure_eq_of_fin_marginals_eq
-- No memories yet, explore from scratch
-- [After 30 minutes of exploration]
-- ✅ Success with π-system uniqueness approach

Store: ProofPattern "pi_system_uniqueness"
  - Works for: measure equality via finite marginals
  - Tactics: [isPiSystem, generateFrom_eq, measure_eq_on_piSystem]
  - Confidence: 0.9
```

**Session 2: Similar theorem (weeks later)**
```lean
-- Proving: fullyExchangeable_via_pathLaw
-- Goal: Show two measures equal
-- System: "Similar to measure_eq_of_fin_marginals_eq"
--         Retrieve memory: pi_system_uniqueness pattern
--         Suggestion: "Try isPiSystem approach?"

-- ✅ Success in 5 minutes using remembered pattern
```

**Session 3: Avoiding failure**
```lean
-- Proving: condIndep_of_condExp_eq
-- About to: simp only [condExp_indicator, mul_comm]
-- ⚠️ Memory: This causes infinite loop (stored Session 1)
--          Alternative: simp only [condExp_indicator], then ring

-- Avoid 20-minute debugging session by using memory
```

## Configuration

### Memory Server Setup

Ensure MCP memory server is configured:

```json
// In Claude Desktop config
{
  "mcpServers": {
    "memory": {
      "command": "npx",
      "args": ["-y", "@modelcontextprotocol/server-memory"]
    }
  }
}
```

### Project-Specific Settings

Memories are automatically scoped by project path. To work across multiple projects:

**Same formalization, different repos:**
```
# Link memories using project aliases
# (Future enhancement - not yet implemented)
```

**Sharing memories with team:**
```
# Export/import functionality
# (Future enhancement - not yet implemented)
```

## Integration with Automation Scripts

Memories enhance script usage:

**proof_templates.sh:**
- Retrieve project-specific template preferences
- Include common proof patterns in scaffolding

**suggest_tactics.sh:**
- Prioritize tactics that succeeded in this project
- Warn about tactics with known issues

**sorry_analyzer.py:**
- Link sorries to similar completed proofs
- Suggest approaches based on memory

## Limitations and Caveats

**What memories DON'T replace:**
- Mathematical understanding
- Lean type system knowledge
- mathlib API documentation
- Formal verification principles

**Potential issues:**
- Stale memories if project evolves significantly
- Over-fitting to specific project patterns
- Memory bloat if not maintained
- Cross-project contamination if scoping fails

**Mitigation:**
- Regular review of stored memories
- Confidence scoring and aging
- Strict project-path scoping
- User control over memory operations

## Future Enhancements

**Planned features:**
- Memory visualization dashboard
- Pattern mining across projects
- Collaborative memory sharing
- Automated memory pruning
- Integration with git history
- Cross-project pattern detection (with user consent)

## See Also

- **lean4-theorem-proving skill** - Core workflows and automation
- **MCP memory server docs** - https://modelcontextprotocol.io/docs/getting-started/intro
- **references/memory-patterns.md** - Detailed memory operation examples