From f90974a9612074a0d2e5bd1424c5bc2a37a15bfc Mon Sep 17 00:00:00 2001 From: Zhongwei Li Date: Sat, 29 Nov 2025 18:03:33 +0800 Subject: [PATCH] Initial commit --- .claude-plugin/plugin.json | 12 + README.md | 3 + plugin.lock.json | 53 ++ skills/lean4-memories/SKILL.md | 443 +++++++++++++ .../references/memory-patterns.md | 602 ++++++++++++++++++ .../lean4-memories/scripts/memory_helper.py | 316 +++++++++ 6 files changed, 1429 insertions(+) create mode 100644 .claude-plugin/plugin.json create mode 100644 README.md create mode 100644 plugin.lock.json create mode 100644 skills/lean4-memories/SKILL.md create mode 100644 skills/lean4-memories/references/memory-patterns.md create mode 100644 skills/lean4-memories/scripts/memory_helper.py diff --git a/.claude-plugin/plugin.json b/.claude-plugin/plugin.json new file mode 100644 index 0000000..a91c236 --- /dev/null +++ b/.claude-plugin/plugin.json @@ -0,0 +1,12 @@ +{ + "name": "lean4-memories", + "description": "Persistent learning across Lean 4 sessions (patterns, dead-ends, conventions)", + "version": "1.0.0", + "author": { + "name": "Cameron Freer", + "email": "cameronfreer@gmail.com" + }, + "skills": [ + "./skills" + ] +} \ No newline at end of file diff --git a/README.md b/README.md new file mode 100644 index 0000000..aa70242 --- /dev/null +++ b/README.md @@ -0,0 +1,3 @@ +# lean4-memories + +Persistent learning across Lean 4 sessions (patterns, dead-ends, conventions) diff --git a/plugin.lock.json b/plugin.lock.json new file mode 100644 index 0000000..81061e4 --- /dev/null +++ b/plugin.lock.json @@ -0,0 +1,53 @@ +{ + "$schema": "internal://schemas/plugin.lock.v1.json", + "pluginId": "gh:cameronfreer/lean4-skills:plugins/lean4-memories", + "normalized": { + "repo": null, + "ref": "refs/tags/v20251128.0", + "commit": "560db6c7a41a418ec395faeaa876ab2609d8ba76", + "treeHash": "a2abdcf92dec73c208d45ab9adba9dc693721af31794a312d862fcc0a29c602e", + "generatedAt": "2025-11-28T10:14:29.514481Z", + "toolVersion": "publish_plugins.py@0.2.0" + }, + "origin": { + "remote": "git@github.com:zhongweili/42plugin-data.git", + "branch": "master", + "commit": "aa1497ed0949fd50e99e70d6324a29c5b34f9390", + "repoRoot": "/Users/zhongweili/projects/openmind/42plugin-data" + }, + "manifest": { + "name": "lean4-memories", + "description": "Persistent learning across Lean 4 sessions (patterns, dead-ends, conventions)", + "version": "1.0.0" + }, + "content": { + "files": [ + { + "path": "README.md", + "sha256": "f32b23537a71bfd92ff5ca6fc21381a758397014a5bb8307810e4fb7297b9ac3" + }, + { + "path": ".claude-plugin/plugin.json", + "sha256": "524ad68f0652b61a372d58af2ff7fc98c2788888f0fd9f75c4b64dd18d024399" + }, + { + "path": "skills/lean4-memories/SKILL.md", + "sha256": "158e14b3e8a10b5a09eecda01d3a83fe4fade2ceca0272d78e4946563b2450bd" + }, + { + "path": "skills/lean4-memories/references/memory-patterns.md", + "sha256": "902f10dceccc914fddb384867cf96a263cbc0331cdee4a9b2090916350e0da7e" + }, + { + "path": "skills/lean4-memories/scripts/memory_helper.py", + "sha256": "74333912f6e136899a7af471728258e243f7ae9e4239cfef3d39c11a048f103a" + } + ], + "dirSha256": "a2abdcf92dec73c208d45ab9adba9dc693721af31794a312d862fcc0a29c602e" + }, + "security": { + "scannedAt": null, + "scannerVersion": null, + "flags": [] + } +} \ No newline at end of file diff --git a/skills/lean4-memories/SKILL.md b/skills/lean4-memories/SKILL.md new file mode 100644 index 0000000..4e3f924 --- /dev/null +++ b/skills/lean4-memories/SKILL.md @@ -0,0 +1,443 @@ +--- +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 diff --git a/skills/lean4-memories/references/memory-patterns.md b/skills/lean4-memories/references/memory-patterns.md new file mode 100644 index 0000000..b3dbc9b --- /dev/null +++ b/skills/lean4-memories/references/memory-patterns.md @@ -0,0 +1,602 @@ +# Memory Patterns and Examples + +This document provides detailed examples of memory operations for the lean4-memories skill. + +## Memory Entity Schemas + +### ProofPattern Entity + +```json +{ + "entity_type": "ProofPattern", + "name": "pi_system_uniqueness_for_measures", + "attributes": { + "project": "/Users/freer/work/exch-repos/exchangeability-cursor", + "skill": "lean4-memories", + "goal_pattern": "Show two measures equal via finite marginals", + "goal_type_signature": "μ₁ = μ₂", + "hypothesis_patterns": [ + "∀ n, μ₁.map (prefixProj n) = μ₂.map (prefixProj n)" + ], + "tactics_sequence": [ + "apply measure_eq_of_fin_marginals_eq", + "intro n", + "simp [prefixProj]" + ], + "helper_lemmas": [ + "isPiSystem_prefixCylinders", + "generateFrom_prefixCylinders", + "measure_eq_on_piSystem" + ], + "domain": "measure_theory", + "difficulty": "medium", + "lines_of_proof": 54, + "confidence": 0.9, + "file": "Exchangeability/Core.lean", + "theorem_name": "measure_eq_of_fin_marginals_eq", + "success_count": 3, + "timestamp": "2025-10-19T14:30:00Z" + }, + "relations": [ + {"type": "uses", "target": "isPiSystem_prefixCylinders"}, + {"type": "similar_to", "target": "fullyExchangeable_via_pathLaw"} + ] +} +``` + +### FailedApproach Entity + +```json +{ + "entity_type": "FailedApproach", + "name": "simp_condExp_mul_comm_loop", + "attributes": { + "project": "/Users/freer/work/exch-repos/exchangeability-cursor", + "skill": "lean4-memories", + "failed_tactic": "simp only [condExp_indicator, mul_comm]", + "error_type": "infinite_loop", + "error_message": "deep recursion was detected", + "context": "Conditional expectation with indicator function", + "goal_pattern": "condExp μ m (indicator S f) = ...", + "file": "Exchangeability/DeFinetti/ViaL2.lean", + "line": 2830, + "alternative_approach": "simp only [condExp_indicator], then use ring", + "alternative_success": true, + "time_wasted": "20 minutes", + "confidence": 0.95, + "timestamp": "2025-10-17T09:15:00Z" + }, + "relations": [ + {"type": "avoided_in", "target": "condIndep_of_condExp_eq"} + ] +} +``` + +### ProjectConvention Entity + +```json +{ + "entity_type": "ProjectConvention", + "name": "measure_theory_instance_declaration", + "attributes": { + "project": "/Users/freer/work/exch-repos/exchangeability-cursor", + "skill": "lean4-memories", + "convention_type": "proof_structure", + "pattern": "haveI : MeasurableSpace Ω := inferInstance", + "description": "All measure theory proofs require explicit MeasurableSpace instance", + "domain": "measure_theory", + "frequency": 15, + "files": [ + "Exchangeability/DeFinetti/ViaL2.lean", + "Exchangeability/Core.lean", + "Exchangeability/Contractability.lean" + ], + "confidence": 0.95, + "timestamp": "2025-10-15T10:00:00Z" + } +} +``` + +### UserPreference Entity + +```json +{ + "entity_type": "UserPreference", + "name": "verbose_script_output", + "attributes": { + "project": "/Users/freer/work/exch-repos/exchangeability-cursor", + "skill": "lean4-memories", + "preference_type": "script_usage", + "setting": "verbose_output", + "value": true, + "context": "User prefers --verbose flag for all automation scripts", + "scripts_affected": [ + "search_mathlib.sh", + "find_instances.sh", + "smart_search.sh" + ], + "confidence": 0.8, + "timestamp": "2025-10-10T16:20:00Z" + } +} +``` + +### TheoremDependency Entity + +```json +{ + "entity_type": "TheoremDependency", + "name": "permutation_extension_lemma_usage", + "attributes": { + "project": "/Users/freer/work/exch-repos/exchangeability-cursor", + "skill": "lean4-memories", + "helper_theorem": "exists_perm_extending_strictMono", + "dependent_theorems": [ + "exchangeable_iff_contractable", + "fullyExchangeable_iff_exchangeable" + ], + "usage_pattern": "Extend finite permutation to full permutation", + "domain": "combinatorics", + "importance": "high", + "confidence": 1.0, + "timestamp": "2025-10-12T11:00:00Z" + }, + "relations": [ + {"type": "critical_for", "target": "exchangeable_iff_contractable"} + ] +} +``` + +## Storage Operation Examples + +### Example 1: Store Successful Proof Pattern + +**Scenario:** Just completed proof of `condIndep_iff_condexp_eq` using conditional expectation uniqueness. + +**Storage operation:** +```python +# Pseudocode for MCP memory operation +memory.create_entity( + entity_type="ProofPattern", + name="condExp_unique_for_conditional_independence", + content={ + "project": os.getcwd(), # /Users/freer/work/exch-repos/exchangeability-cursor + "skill": "lean4-memories", + "goal_pattern": "Prove conditional independence via conditional expectation equality", + "goal_type": "CondIndep X Y m ↔ condExp m X = condExp m Y", + "tactics_sequence": [ + "apply condExp_unique", + "intro s hs", + "show_ae_eq", + "measurability" + ], + "helper_lemmas": [ + "condExp_unique", + "ae_eq_condExp_of_forall_setIntegral_eq", + "setIntegral_condExp" + ], + "domain": "probability_theory", + "subdomain": "conditional_independence", + "difficulty": "large", + "lines_of_proof": 85, + "sorry_count": 0, + "confidence": 0.9, + "file": "Exchangeability/DeFinetti/ViaL2.lean", + "theorem_name": "condIndep_iff_condexp_eq", + "timestamp": datetime.now().isoformat() + } +) + +memory.create_relations([ + {"source": "condIndep_iff_condexp_eq", "type": "uses", "target": "condExp_unique"}, + {"source": "condIndep_iff_condexp_eq", "type": "similar_to", "target": "condProb_eq_of_eq_on_pi_system"} +]) +``` + +### Example 2: Store Failed Approach + +**Scenario:** Attempted to use `tsum_congr` with `condExp` but got type mismatch. + +**Storage operation:** +```python +memory.create_entity( + entity_type="FailedApproach", + name="tsum_condExp_direct_exchange", + content={ + "project": os.getcwd(), + "skill": "lean4-memories", + "failed_tactic": "apply tsum_congr; intro i; rw [condExp_indicator]", + "error_type": "type_mismatch", + "error_message": "expected condExp to be measurable, but got ae-measurable", + "context": "Trying to exchange tsum and condExp directly", + "goal_pattern": "condExp (∑' i, f i) = ∑' i, condExp (f i)", + "why_failed": "condExp output is only ae-measurable, not point-wise measurable", + "file": "Exchangeability/DeFinetti/ViaL2.lean", + "line": 643, + "alternative_approach": "Use restricted measure trick: switch to μ.restrict S", + "alternative_detail": "integral_condExp on restricted measure with set = univ", + "alternative_success": true, + "time_wasted": "45 minutes", + "learning": "Cannot exchange condExp with series directly; need measure restriction", + "confidence": 0.95, + "timestamp": datetime.now().isoformat() + } +) +``` + +### Example 3: Store Project Convention + +**Scenario:** Observed consistent pattern of hypothesis naming across 10+ files. + +**Storage operation:** +```python +memory.create_entity( + entity_type="ProjectConvention", + name="hypothesis_naming_pattern", + content={ + "project": os.getcwd(), + "skill": "lean4-memories", + "convention_type": "naming", + "category": "hypotheses", + "pattern": "h{property_name}", + "examples": [ + "hExchangeable : Exchangeable μ X", + "hMeasurable : Measurable f", + "hIntegrable : Integrable f μ", + "hContract : Contractable μ X" + ], + "description": "Hypotheses prefixed with 'h' followed by property name", + "exceptions": [ + "ih for induction hypothesis", + "hs for set membership (h_s avoided)" + ], + "frequency": 120, + "files_surveyed": 15, + "confidence": 0.95, + "timestamp": datetime.now().isoformat() + } +) +``` + +### Example 4: Store User Preference + +**Scenario:** User consistently requests ripgrep output format. + +**Storage operation:** +```python +memory.create_entity( + entity_type="UserPreference", + name="search_tool_preference", + content={ + "project": os.getcwd(), + "skill": "lean4-memories", + "preference_type": "tool_usage", + "tool": "search_mathlib.sh", + "setting": "output_format", + "preferred_value": "with_context", + "reasoning": "User wants to see surrounding code for search results", + "explicit_request": true, + "frequency": 8, + "confidence": 0.9, + "timestamp": datetime.now().isoformat() + } +) +``` + +## Retrieval Operation Examples + +### Example 1: Retrieve Similar Proof Patterns + +**Scenario:** About to prove `fullyExchangeable_iff_X` which requires showing measure equality. + +**Retrieval query:** +```python +# Query for similar patterns +results = memory.search_entities( + query="measure equality finite marginals", + entity_type="ProofPattern", + filters={ + "project": os.getcwd(), + "skill": "lean4-memories", + "confidence": {">=": 0.7} + }, + limit=5 +) + +# Expected result: +# ProofPattern: pi_system_uniqueness_for_measures +# - Tactics: [apply measure_eq_of_fin_marginals_eq, ...] +# - Confidence: 0.9 +# - Success count: 3 + +# Suggested action: +# "This goal is similar to measure_eq_of_fin_marginals_eq" +# "Try π-system uniqueness approach: apply measure_eq_of_fin_marginals_eq" +``` + +### Example 2: Check for Known Failures + +**Scenario:** About to apply `simp only [condExp_indicator, mul_comm]`. + +**Retrieval query:** +```python +# Query for known issues with this tactic +results = memory.search_entities( + query="simp condExp_indicator mul_comm", + entity_type="FailedApproach", + filters={ + "project": os.getcwd(), + "skill": "lean4-memories" + } +) + +# Expected result: +# FailedApproach: simp_condExp_mul_comm_loop +# - Error: infinite_loop +# - Alternative: simp only [condExp_indicator], then ring + +# Suggested action: +# ⚠️ WARNING: This tactic combination causes infinite loop +# Alternative approach: Use simp only [condExp_indicator] without mul_comm, then ring +``` + +### Example 3: Retrieve Project Conventions + +**Scenario:** Starting new theorem in measure theory file. + +**Retrieval query:** +```python +# Query for measure theory conventions +results = memory.search_entities( + query="measure theory proof structure", + entity_type="ProjectConvention", + filters={ + "project": os.getcwd(), + "skill": "lean4-memories", + "domain": "measure_theory" + } +) + +# Expected result: +# ProjectConvention: measure_theory_instance_declaration +# - Pattern: haveI : MeasurableSpace Ω := inferInstance +# - Frequency: 15 occurrences + +# Suggested action: +# "Based on project conventions, start with:" +# haveI : MeasurableSpace Ω := inferInstance +``` + +### Example 4: Find Helpful Lemmas + +**Scenario:** Stuck on proof, need helper lemmas. + +**Retrieval query:** +```python +# Query for theorems that helped with similar goals +results = memory.search_entities( + query="conditional expectation uniqueness", + entity_type="TheoremDependency", + filters={ + "project": os.getcwd(), + "skill": "lean4-memories", + "domain": "probability_theory" + } +) + +# Expected result: +# TheoremDependency: condExp_unique_usage_pattern +# - Helper: condExp_unique +# - Used in: [condIndep_iff_condexp_eq, condProb_eq_of_eq_on_pi_system] +# - Pattern: "Test equality on measurable sets via integrals" + +# Suggested action: +# "Consider using condExp_unique - it helped with similar proofs" +# "Pattern: Show ae_eq by testing on measurable sets" +``` + +## Memory Maintenance Examples + +### Update Memory with New Success + +**Scenario:** Used `pi_system_uniqueness` pattern successfully again. + +```python +# Retrieve existing memory +pattern = memory.get_entity("pi_system_uniqueness_for_measures") + +# Update success count and confidence +pattern.attributes["success_count"] += 1 +pattern.attributes["confidence"] = min(1.0, pattern.attributes["confidence"] + 0.05) +pattern.attributes["last_used"] = datetime.now().isoformat() + +memory.update_entity(pattern) +``` + +### Deprecate Outdated Memory + +**Scenario:** Found better approach than stored pattern. + +```python +# Mark old pattern as deprecated +old_pattern = memory.get_entity("old_approach_name") +old_pattern.attributes["deprecated"] = true +old_pattern.attributes["deprecation_reason"] = "Better approach found: new_approach_name" +old_pattern.attributes["replaced_by"] = "new_approach_name" + +memory.update_entity(old_pattern) + +# Store new pattern +memory.create_entity( + entity_type="ProofPattern", + name="new_approach_name", + content={...} +) +``` + +### Prune Low-Confidence Memories + +**Scenario:** Periodic cleanup of unreliable memories. + +```python +# Query for low-confidence, old memories +candidates = memory.search_entities( + entity_type="ProofPattern", + filters={ + "project": os.getcwd(), + "skill": "lean4-memories", + "confidence": {"<": 0.5}, + "timestamp": {"<": one_month_ago} + } +) + +# Review and delete if not used +for pattern in candidates: + if pattern.attributes["success_count"] == 0: + memory.delete_entity(pattern.name) +``` + +## Integration Patterns + +### Pattern 1: Pre-Proof Memory Check + +Before starting a proof, check memories: + +```python +def pre_proof_memory_check(goal_description): + # 1. Check for similar successful patterns + similar = memory.search_entities( + query=goal_description, + entity_type="ProofPattern", + filters={"project": os.getcwd(), "confidence": {">=": 0.7}} + ) + + # 2. Check for known failures with this goal type + failures = memory.search_entities( + query=goal_description, + entity_type="FailedApproach", + filters={"project": os.getcwd()} + ) + + # 3. Get relevant conventions + conventions = memory.search_entities( + query=extract_domain(goal_description), + entity_type="ProjectConvention", + filters={"project": os.getcwd()} + ) + + return { + "similar_proofs": similar, + "known_failures": failures, + "conventions": conventions + } +``` + +### Pattern 2: Post-Proof Memory Storage + +After completing a proof, store the pattern: + +```python +def post_proof_memory_store(proof_info): + # Only store non-trivial proofs + if proof_info["lines"] < 10: + return + + # Only store if confidence is reasonable + if proof_info["sorry_count"] > 0: + confidence = 0.5 + elif proof_info["warnings"] > 0: + confidence = 0.7 + else: + confidence = 0.9 + + memory.create_entity( + entity_type="ProofPattern", + name=generate_pattern_name(proof_info), + content={ + "project": os.getcwd(), + "skill": "lean4-memories", + "goal_pattern": proof_info["goal"], + "tactics_sequence": proof_info["tactics"], + "helper_lemmas": proof_info["lemmas_used"], + "difficulty": estimate_difficulty(proof_info["lines"]), + "confidence": confidence, + **proof_info + } + ) +``` + +### Pattern 3: Tactic Suggestion with Memory + +Enhance tactic suggestions with memory: + +```python +def suggest_tactics_with_memory(goal): + # Get base suggestions from goal pattern + base_suggestions = analyze_goal_pattern(goal) + + # Enhance with memory + memory_patterns = memory.search_entities( + query=goal, + entity_type="ProofPattern", + filters={"project": os.getcwd(), "confidence": {">=": 0.7}} + ) + + # Prioritize tactics from successful memories + for pattern in memory_patterns: + for tactic in pattern.attributes["tactics_sequence"]: + if tactic not in base_suggestions: + base_suggestions.append({ + "tactic": tactic, + "source": "memory", + "confidence": pattern.attributes["confidence"] + }) + + # Filter out known failures + failures = memory.search_entities( + query=goal, + entity_type="FailedApproach", + filters={"project": os.getcwd()} + ) + + for failure in failures: + base_suggestions = [ + s for s in base_suggestions + if s["tactic"] != failure.attributes["failed_tactic"] + ] + + return sorted(base_suggestions, key=lambda x: x.get("confidence", 0.5), reverse=True) +``` + +## Best Practices + +### When to Store Memories + +**DO store:** +- ✅ Proofs with >10 lines (non-trivial) +- ✅ Approaches that failed after >10 minutes of trying +- ✅ Patterns observed 3+ times +- ✅ Project-specific insights not in mathlib docs + +**DON'T store:** +- ❌ One-line proofs (rfl, simp, exact) +- ❌ Obvious applications of standard lemmas +- ❌ Temporary hacks or workarounds +- ❌ General Lean knowledge + +### Confidence Scoring Guidelines + +- **0.9-1.0:** Clean proof, no warnings, used successfully multiple times +- **0.7-0.9:** Works well, minor issues or single use +- **0.5-0.7:** Works but has problems, needs refinement +- **0.3-0.5:** Hacky solution, use only if nothing else works +- **0.0-0.3:** Experimental, likely needs replacement + +### Memory Scoping Guidelines + +Always scope by: +1. **Project path** (absolute path to repository) +2. **Skill** ("lean4-memories") +3. **Entity type** (ProofPattern, FailedApproach, etc.) + +Never mix memories across projects unless explicitly linked. diff --git a/skills/lean4-memories/scripts/memory_helper.py b/skills/lean4-memories/scripts/memory_helper.py new file mode 100644 index 0000000..3059415 --- /dev/null +++ b/skills/lean4-memories/scripts/memory_helper.py @@ -0,0 +1,316 @@ +#!/usr/bin/env python3 +""" +Memory Helper for Lean 4 Formalization + +This script provides convenient wrappers for MCP memory operations +specific to Lean 4 theorem proving workflows. + +Usage: + # Store a successful proof pattern + ./memory_helper.py store-pattern --goal "..." --tactics "..." --confidence 0.9 + + # Retrieve similar patterns + ./memory_helper.py find-patterns --query "conditional expectation" + + # Store a failed approach + ./memory_helper.py store-failure --tactic "simp only [...]" --error "infinite loop" + + # Check for known failures + ./memory_helper.py check-failure --tactic "simp only [...]" + +Note: This script assumes MCP memory server is configured and available. + It provides a CLI interface but is primarily designed to be used + programmatically by Claude during theorem proving sessions. +""" + +import os +import sys +import json +import argparse +from datetime import datetime +from pathlib import Path +from typing import Dict, List, Optional, Any + +# Note: In actual usage with MCP, these would use the MCP client API +# For now, this is a template showing the structure and interface + +def get_project_root() -> str: + """Get absolute path to current project (git root or cwd).""" + cwd = os.getcwd() + + # Try to find git root + current = Path(cwd) + while current != current.parent: + if (current / '.git').exists(): + return str(current) + current = current.parent + + # Fall back to cwd + return cwd + +def estimate_difficulty(lines: int) -> str: + """Estimate proof difficulty from line count.""" + if lines <= 10: + return "small" + elif lines <= 50: + return "medium" + elif lines <= 100: + return "large" + else: + return "huge" + +def store_proof_pattern(args: argparse.Namespace) -> None: + """Store a successful proof pattern in memory.""" + + project = get_project_root() + + entity = { + "entity_type": "ProofPattern", + "name": args.name or f"pattern_{datetime.now().strftime('%Y%m%d_%H%M%S')}", + "content": { + "project": project, + "skill": "lean4-memories", + "goal_pattern": args.goal, + "tactics_sequence": args.tactics.split(",") if isinstance(args.tactics, str) else args.tactics, + "helper_lemmas": args.lemmas.split(",") if args.lemmas else [], + "domain": args.domain or "general", + "difficulty": args.difficulty or estimate_difficulty(args.lines or 20), + "lines_of_proof": args.lines or 0, + "confidence": args.confidence, + "file": args.file or "", + "theorem_name": args.theorem or "", + "success_count": 1, + "timestamp": datetime.now().isoformat() + } + } + + # In actual MCP usage, this would call: + # mcp_client.create_entity(**entity) + + print(f"Would store ProofPattern: {entity['name']}") + print(json.dumps(entity, indent=2)) + print("\n✅ Pattern stored successfully (simulation)") + +def find_similar_patterns(args: argparse.Namespace) -> None: + """Find similar proof patterns from memory.""" + + project = get_project_root() + + query_params = { + "query": args.query, + "entity_type": "ProofPattern", + "filters": { + "project": project, + "skill": "lean4-memories", + "confidence": {">=": args.min_confidence} + }, + "limit": args.limit + } + + # In actual MCP usage, this would call: + # results = mcp_client.search_entities(**query_params) + + print(f"Would query for patterns: {args.query}") + print(json.dumps(query_params, indent=2)) + print("\n📋 Results would appear here (simulation)") + print("Example result:") + print({ + "name": "pi_system_uniqueness", + "goal_pattern": "Show measures equal via finite marginals", + "tactics": ["apply measure_eq_of_fin_marginals_eq", "intro n"], + "confidence": 0.9 + }) + +def store_failed_approach(args: argparse.Namespace) -> None: + """Store a failed approach to avoid repeating.""" + + project = get_project_root() + + entity = { + "entity_type": "FailedApproach", + "name": args.name or f"failure_{datetime.now().strftime('%Y%m%d_%H%M%S')}", + "content": { + "project": project, + "skill": "lean4-memories", + "failed_tactic": args.tactic, + "error_type": args.error_type or "unknown", + "error_message": args.error, + "context": args.context or "", + "goal_pattern": args.goal or "", + "file": args.file or "", + "line": args.line or 0, + "alternative_approach": args.alternative or "", + "time_wasted": args.time_wasted or "", + "confidence": 0.95, # High confidence in failures + "timestamp": datetime.now().isoformat() + } + } + + # In actual MCP usage, this would call: + # mcp_client.create_entity(**entity) + + print(f"Would store FailedApproach: {entity['name']}") + print(json.dumps(entity, indent=2)) + print("\n✅ Failure stored successfully (simulation)") + print("⚠️ This approach will be flagged in future sessions") + +def check_for_failure(args: argparse.Namespace) -> None: + """Check if a tactic is known to fail.""" + + project = get_project_root() + + query_params = { + "query": args.tactic, + "entity_type": "FailedApproach", + "filters": { + "project": project, + "skill": "lean4-memories" + } + } + + # In actual MCP usage, this would call: + # results = mcp_client.search_entities(**query_params) + + print(f"Checking if tactic is known to fail: {args.tactic}") + print(json.dumps(query_params, indent=2)) + print("\n🔍 Check results (simulation):") + print("✅ No known failures for this tactic") + # Or if found: + # print("⚠️ WARNING: This tactic causes infinite loop (stored 2025-10-17)") + +def store_convention(args: argparse.Namespace) -> None: + """Store a project convention.""" + + project = get_project_root() + + entity = { + "entity_type": "ProjectConvention", + "name": args.name or f"convention_{datetime.now().strftime('%Y%m%d_%H%M%S')}", + "content": { + "project": project, + "skill": "lean4-memories", + "convention_type": args.type or "general", + "pattern": args.pattern, + "description": args.description, + "domain": args.domain or "general", + "frequency": args.frequency or 1, + "confidence": args.confidence, + "timestamp": datetime.now().isoformat() + } + } + + print(f"Would store ProjectConvention: {entity['name']}") + print(json.dumps(entity, indent=2)) + print("\n✅ Convention stored successfully (simulation)") + +def list_memories(args: argparse.Namespace) -> None: + """List all memories for current project.""" + + project = get_project_root() + + print(f"📁 Project: {project}") + print(f"🔍 Memory type: {args.type or 'all'}") + print("\nWould list memories here (simulation)") + print("\nExample memories:") + print("- ProofPattern: pi_system_uniqueness (confidence: 0.9, used: 3 times)") + print("- FailedApproach: simp_condExp_loop (avoided infinite loop)") + print("- ProjectConvention: hypothesis_naming (h_ prefix)") + +def export_memories(args: argparse.Namespace) -> None: + """Export memories to JSON file for sharing.""" + + project = get_project_root() + output_file = args.output or "lean4_memories_export.json" + + print(f"Would export memories from {project} to {output_file}") + print("✅ Export complete (simulation)") + +def main(): + parser = argparse.ArgumentParser( + description="Memory Helper for Lean 4 Formalization", + formatter_class=argparse.RawDescriptionHelpFormatter, + epilog=__doc__ + ) + + subparsers = parser.add_subparsers(dest='command', help='Commands') + + # Store proof pattern + pattern_parser = subparsers.add_parser('store-pattern', help='Store successful proof pattern') + pattern_parser.add_argument('--name', help='Pattern name') + pattern_parser.add_argument('--goal', required=True, help='Goal description') + pattern_parser.add_argument('--tactics', required=True, help='Comma-separated tactics') + pattern_parser.add_argument('--lemmas', help='Comma-separated helper lemmas') + pattern_parser.add_argument('--domain', help='Domain (measure_theory, probability, etc.)') + pattern_parser.add_argument('--difficulty', choices=['small', 'medium', 'large', 'huge']) + pattern_parser.add_argument('--lines', type=int, help='Lines of proof') + pattern_parser.add_argument('--confidence', type=float, default=0.8, help='Confidence (0.0-1.0)') + pattern_parser.add_argument('--file', help='File name') + pattern_parser.add_argument('--theorem', help='Theorem name') + + # Find patterns + find_parser = subparsers.add_parser('find-patterns', help='Find similar proof patterns') + find_parser.add_argument('--query', required=True, help='Search query') + find_parser.add_argument('--min-confidence', type=float, default=0.7, help='Minimum confidence') + find_parser.add_argument('--limit', type=int, default=5, help='Max results') + + # Store failure + failure_parser = subparsers.add_parser('store-failure', help='Store failed approach') + failure_parser.add_argument('--name', help='Failure name') + failure_parser.add_argument('--tactic', required=True, help='Failed tactic') + failure_parser.add_argument('--error', required=True, help='Error message') + failure_parser.add_argument('--error-type', help='Error type (infinite_loop, type_mismatch, etc.)') + failure_parser.add_argument('--context', help='Context description') + failure_parser.add_argument('--goal', help='Goal pattern') + failure_parser.add_argument('--file', help='File name') + failure_parser.add_argument('--line', type=int, help='Line number') + failure_parser.add_argument('--alternative', help='Alternative that worked') + failure_parser.add_argument('--time-wasted', help='Time wasted (e.g., "20 minutes")') + + # Check failure + check_parser = subparsers.add_parser('check-failure', help='Check if tactic is known to fail') + check_parser.add_argument('--tactic', required=True, help='Tactic to check') + + # Store convention + convention_parser = subparsers.add_parser('store-convention', help='Store project convention') + convention_parser.add_argument('--name', help='Convention name') + convention_parser.add_argument('--type', help='Convention type') + convention_parser.add_argument('--pattern', required=True, help='Pattern') + convention_parser.add_argument('--description', required=True, help='Description') + convention_parser.add_argument('--domain', help='Domain') + convention_parser.add_argument('--frequency', type=int, help='Observation frequency') + convention_parser.add_argument('--confidence', type=float, default=0.8, help='Confidence') + + # List memories + list_parser = subparsers.add_parser('list', help='List memories for current project') + list_parser.add_argument('--type', help='Filter by type (ProofPattern, FailedApproach, etc.)') + + # Export memories + export_parser = subparsers.add_parser('export', help='Export memories to JSON') + export_parser.add_argument('--output', help='Output file (default: lean4_memories_export.json)') + + args = parser.parse_args() + + if not args.command: + parser.print_help() + sys.exit(1) + + # Dispatch to appropriate handler + handlers = { + 'store-pattern': store_proof_pattern, + 'find-patterns': find_similar_patterns, + 'store-failure': store_failed_approach, + 'check-failure': check_for_failure, + 'store-convention': store_convention, + 'list': list_memories, + 'export': export_memories + } + + handler = handlers.get(args.command) + if handler: + handler(args) + else: + print(f"Unknown command: {args.command}") + sys.exit(1) + +if __name__ == '__main__': + main()