lean4-memories

What problem does it solve?

This Skill eliminates the frustration of rediscovering proof approaches across sessions by maintaining persistent memory of successful patterns, failed attempts, and project conventions.

Core Features & Use Cases

• Persistent Learning: Remember successful proof strategies and avoid known dead-ends across multiple work sessions.
• Project-Specific Expertise: Accumulate domain knowledge and coding conventions specific to your formalization project.
• Use Case: Imagine you spent 30 minutes finding a successful π-system approach for measure equality. This Skill remembers that pattern so when you encounter similar goals weeks later, it suggests the proven approach in minutes.

Quick Start

Use the lean4-memories skill to retrieve similar proof patterns for the current theorem goal in your Lean 4 project.