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
npxskills add benchflow-ai/skillsbench--skill lean4-memoriesLoading…
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.
This skill applies when working on Lean 4 formalization projects, especially:
Especially important when:
All memories are scoped by:
lean4-memoriesExample scoping:
Project: /Users/freer/work/exch-repos/exchangeability-cursor
Skill: lean4-memories
Entity: ProofPattern:condExp_unique_pattern
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
After successful proof:
-- Just proved: exchangeable_iff_fullyExchangeable
-- Store the successful pattern
Store:
exchangeable X ↔ fullyExchangeable X[apply measure_eq_of_fin_marginals_eq, intro, simp][prefixCylinder_measurable, isPiSystem_prefixCylinders]After failed approach:
-- Attempted: simp only [condExp_indicator, mul_comm]
-- Result: infinite loop, build timeout
Store:
simp only [condExp_indicator, mul_comm]Project conventions observed:
-- Pattern: All measure theory proofs start with haveI
haveI : MeasurableSpace Ω := inferInstance
Store:
haveI : MeasurableSpace ΩStarting new proof session:
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
The lean4-memories skill complements (doesn't replace) lean4-theorem-proving:
lean4-theorem-proving provides:
lean4-memories adds:
Use together:
After completing a proof, store the pattern using MCP memory:
What to capture:
When to store:
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}
When an approach fails (error, loop, timeout), store to avoid repeating:
What to capture:
When to store:
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}
Track consistent patterns that emerge:
What to capture:
When to store:
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"}
)
DO store:
DON'T store:
Confidence scoring:
Aging:
Pruning:
Users can:
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
Ensure MCP memory server is configured:
// In Claude Desktop config
{
"mcpServers": {
"memory": {
"command": "npx",
"args": ["-y", "@modelcontextprotocol/server-memory"]
}
}
}
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)
Memories enhance script usage:
proof_templates.sh:
suggest_tactics.sh:
sorry_analyzer.py:
What memories DON'T replace:
Potential issues:
Mitigation:
Planned features:
Create or update AgentSkills. Use when designing, structuring, or packaging skills with scripts, references, and assets.
Create or update AgentSkills. Use when designing, structuring, or packaging skills with scripts, references, and assets.
Set up and use 1Password CLI (op). Use when installing the CLI, enabling desktop app integration, signing in (single or multi-account), or reading/injecting/running secrets via op.
CLI to manage emails via IMAP/SMTP. Use `himalaya` to list, read, write, reply, forward, search, and organize emails from the terminal. Supports multiple accounts and message composition with MML (MIME Meta Language).
Create or update AgentSkills. Use when designing, structuring, or packaging skills with scripts, references, and assets.
Create or update AgentSkills. Use when designing, structuring, or packaging skills with scripts, references, and assets.
Set up and use 1Password CLI (op). Use when installing the CLI, enabling desktop app integration, signing in (single or multi-account), or reading/injecting/running secrets via op.
CLI to manage emails via IMAP/SMTP. Use `himalaya` to list, read, write, reply, forward, search, and organize emails from the terminal. Supports multiple accounts and message composition with MML (MIME Meta Language).