用途：用于任何 Lean 4 开发，包括纯数学与应用数学证明、程序验证、mathlib 贡献。核心原则为增量构建、先结构后求解、信任类型检查器；成功标准是 lake build 通过且零 sorry、零自定义 axiom，含 sorry/axiom 的定理只是脚手架而非成果。
主要能力：提供在 Claude Code 中输入的 /lean 系列斜杠命令，涵盖搜索、分析、优化、修复；提供 19 个自动化脚本用于搜索、验证、重构与修复；可选 4 个子代理用于批量任务；可选 Lean LSP 服务器带来约 30 倍更快反馈与即时证明状态；附 18 份参考文档（短语手册、策略、模式、错误、修复、性能等）。
使用方式：遵循四阶段工作流——先用 have 与带注释的 sorry 规划结构，再自底向上构建辅助引理，随后逐个填充 sorry 并在每次后编译，最后通过 haveI/letI 处理类型类实例。查找 mathlib 引理时先搜索再证明，可用 /search-mathlib、LSP 搜索或脚本。常用策略包括 simp only、rw、apply、exact、refine、by_cases、rcases、ext/funext；领域模式涉及 analysis/topology、algebra、measure theory 与 probability。编译失败时用编译器引导修复，先运行自动求解级联（rfl、simp、ring、linarith、nlinarith、omega、exact?、apply?、aesop），再按阶段调用修复代理，最小补丁后重新编译，最多 24 次尝试。
限制与注意：提交前必须 lake build 成功；所有 sorry 需附具体策略；新增 axiom 需有消除计划；导入应尽量精简。标准 mathlib axiom 可用 Classical.choice、propext、quot.sound，并用 #print axioms 或 /check-axioms 检查。具体命令路径、脚本细节与安装方式以对应文档为准；资料未提供价格、收费、平台覆盖与效果数据。