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