用途：在 Lean 4 形式化项目中提供跨会话的持久记忆，把无状态的证明辅助变成可积累经验的学习系统。它通过 MCP（Model Context Protocol）记忆服务器保存并检索信息，适用于多会话长期项目、重复出现的证明模式、复杂证明、团队协作和领域知识积累。
主要能力：记忆按项目路径、技能上下文（标记 lean4-memories）和实体类型隔离，避免跨项目污染。支持五类记忆：ProofPattern（成功证明策略，含目标模式、可用策略序列、辅助引理、难度与置信度）、FailedApproach（导致循环、超时或类型错误的死路及替代方案）、ProjectConvention（命名、结构、导入、策略偏好等约定）、UserPreference（工作流偏好）、TheoremDependency（定理间依赖关系）。检索时机包括开始新会话时加载项目约定、遇到相似目标时调取历史模式、尝试某策略前检查已知失败。
使用方式：需确保 MCP memory 服务器已配置，例如在 Claude Desktop 配置中使用 command "npx"、args ["-y", "@modelcontextprotocol/server-memory"]。存储与检索通过 MCP 记忆操作完成，查询可按项目与实体类型过滤。该技能与 lean4-theorem-proving 互补：后者提供通用工作流、mathlib 搜索与自动化脚本，前者提供项目特有的学习模式与历史。
最佳实践：只存储非平凡的成功证明（超过 10 行）、耗费大量时间的失败尝试、多次出现的稳定约定；不存储 rfl、simp 等平凡证明和一次性技巧。使用置信度评分并对旧记忆进行核实与清理。
限制：记忆不能替代数学理解、Lean 类型系统知识、mathlib API 文档和形式化验证原则。项目演进可能导致记忆过时，存在过拟合、记忆膨胀和隔离失效风险。跨仓库别名链接、团队导出/导入等标注为未来增强，尚未实现。具体收费、平台与价格信息暂未提供。