在 Lean 4 中编写可维护证明与库设计时：用自顶向下设计…

适用于在 Lean 4 中证明定理、形式化数学或规格、设计库 API、重构长证明、配置 CI/linter、诊断慢证明或编写自定义 tactic 的场景。

适用场景

解决思路

1. 先设计定义及其 API：优先使用带 junk 值的全函数而非子类型或 Option；新态射类型用带 FunLike 实例的结构体，新子对象类型用 SetLike，性质证明作为结构体字段而非独立的 IsHom 谓词；为每个有多种等价写法的概念选定唯一的 simp 规范形式，所有 API 引理只针对该形式陈述；在定义被使用之前，在同一文件中立即编写 ext、@[simp]、强制转换和单射引理，下游证明只使用 API，绝不使用 unfold 或 show ... from rfl。
2. 构建 sorry 骨架：在项目层面，先用 := sorry 陈述目标定理及其所需引理并让文件编译通过，使每个 sorry 成为独立工作单元；在证明层面，用 sorry 填充 have/suffices/calc 骨架，先让 Lean 接受结构，再逐步填充每一步。
3. 逐个聚焦目标地填充：每个新子目标都用聚焦点 · 加缩进块，绝不留多个未聚焦的活动目标；每个块开头用冗余的 show 陈述其目标（若 show 会改变目标则改用 change）；链式等式/不等式重写用 calc 块并垂直对齐关系符；向前推进用 have，向后归约用 suffices；起草时在非显然 tactic 前用注释标注目标状态，无头工作流中插入 trace_state 或在应关闭目标处故意写 done，然后运行 lake env lean Path/To/File.lean 并复制报告的假设、case 名和目标，证明通过后删除常规探测。
4. 机械验证：运行 lake build 只是底线，因为 sorry 只是警告；用 #print axioms myTheorem 抽查，CI 中用 Lean.collectAxioms 按声明收集公理并断言完整的预期足迹（除非有意放宽，否则为 [propext, Classical.choice, Quot.sound]），绝不用 grep 检查未证明义务；按项目角色选择 lint 并在项目开始时放入 CI，自包含证明从 linter.auxLemma、linter.style.maxHeartbeats、linter.style.multiGoal、linter.style.setOption、linter.style.show 开始，可复用库再加 linter.flexible、linter.style.missingEnd、linter.style.openClassical 和两个 unused*InType 检查，把 nativeDecide 视为信任策略选择，格式和弃用语法检查视为项目风格，确保警告会使构建失败，单独运行 Batteries 的声明级 #lint 检查（包括 simpNF），对照固定的 Mathlib 源码和已知触发夹具验证每个选项；为每个项目特定约定编写自定义 linter（如 @[env_linter]），并遵循空真锚点、证明其能失败、允许列表等工程规则。
5. 按提取阶梯决定何时把证明结构升级为独立引理：提取前先在临时 example 中写出拟议陈述，对裸目标运行 exact? 和 apply?，再尝试类型模式和源码搜索，若已有定理匹配则直接使用，未记录失败搜索不得报告 API 缺口；子论证在同一证明中重复时命名为局部 have；陈述独立有趣或提取能去掉子论证不需要的假设时提取为独立引理（去掉多余假设是更强的触发条件）；证明读起来冗长笨重时拆分，这是 Mathlib 的评审标准且刻意定性、没有行数阈值，有疑问就尝试提取，若片段有干净陈述它就本该是引理。
6. 遵循快速参考规则：下游绝不 unfold 定义，erw 或尾部 rfl 意味着缺少 API；终端 simp 保持未挤压，非终端 simp 改为 simp only [...]；一次只聚焦一个目标；show 不得改变目标；最终代码中不得有 set_option 调试/追踪/分析器或未限定作用域的 maxHeartbeats；引理以 simp 规范形式陈述，用 < 而非 >；只有当结果至少同样可读时才 golf，平凡结果豁免；Fact 实例是局部的，绝不全局；引理名从陈述推导；写辅助引理或声称 API 缺口前先按形状搜索裸目标；一般每行一次 tactic 调用，单行收尾证明是例外；用 collectAxioms/#print axioms 而非 grep 把关 sorry；优先使用以结构而非数字为键的 simp 引理 LHS，每个常量一种写法；在每个使用处用 simp? 重新推导每个 simp only 列表；每个 maxHeartbeats 覆盖都是未证明的声明，相信前先测量；条件 simp 引理浅层触发但深层不触发时提高 maxDischargeDepth（默认 2）；每个项目特定约定从第一天起就在 CI 中有自定义 linter。
7. 拒绝常见借口：编译通过只是底线，只有 Lean 能读的单体 tactic 块会在下次 Mathlib 升级时静默损坏；展开定义比写 API 引理简单会让每个下游 unfold 耦合到实现，第一次重构就全部断裂；挤压每个 simp 对终端调用适得其反，挤压列表会在每次重命名时断裂；更短不等于更好，Mathlib 评审政策是 golf 仅在不妨碍可读性时可行；等工作后再重构为引理时结构已纠缠不清，应先陈述骨架；show 行对内核冗余但对读者和模型必不可少；辅助引理太具体不是理由，若有干净陈述就提取；等库稳定再加 linter 是反的，模式会通过复制传播；检查通过不代表干净，无法失败的检查什么也证明不了；证明慢就提高 maxHeartbeats 是未测量的声明而非修复，应测量并重构定义或分解目标。

适用边界 · 注意事项

• 将 Lean 4 用作通用编程语言（不涉及证明）——本技能主要针对证明和 API 结构
• Coq、Isabelle、Agda 或 Lean 3——约定和 tactic 名称不同，Lean 3 习语（ge_or_gt linting、discrete_field）已过时
• 有自己内部风格的已验证软件 Lean 项目（如规格可追溯性优先的代码库）：Mathlib 约定是社区默认，但应先查看项目的 CONTRIBUTING 并遵从它