zhongwei/gh-cameronfreer-lean4-skills-plugins-lean4-memories
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity
Files
master
gh-cameronfreer-lean4-skill…/skills/lean4-memories/references/memory-patterns.md
Zhongwei Li f90974a961 Initial commit
2025-11-29 18:03:33 +08:00

17 KiB
Raw Permalink Blame History

Memory Patterns and Examples

This document provides detailed examples of memory operations for the lean4-memories skill.

Memory Entity Schemas

ProofPattern Entity

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

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

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

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

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

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

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:

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:

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:

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

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

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

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

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

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

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

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:

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:

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.

Reference in New Issue View Git Blame Copy Permalink