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
SKILL.md
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:
⊢ 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:
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
