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:

-- 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:

-- 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:

-- 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

-- 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)

-- 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

-- 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:

// 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