writing-lean-proofs

Compare original and translation side by side

🇺🇸

Original

English

🇨🇳

Translation

Chinese

Writing Lean Proofs

编写Lean证明

Core principle: design top-down, prove bottom-up. Lean propositions are proof-irrelevant — only a theorem's statement can affect later declarations. Statements are the stable interface; proofs are disposable and freely replaceable. Put design effort into definitions and statements, then fill in proofs against skeletons that already compile (modulo

sorry

适用场景
不适用场景
工作流程
提取阶梯
快速参考
需摒弃的借口
参考资料

结构化Lean 4证明编写与库设计方法，提炼自Mathlib的风格和审阅规范，以及大型形式化项目（如Liquid Tensor Experiment、PFR、费马大定理）的方法论。

核心原则：自上而下设计，自下而上证明。 Lean命题与证明无关——只有定理的陈述会影响后续声明。陈述是稳定的接口；证明是可替换的，可自由修改。将设计精力投入到定义和陈述中，然后针对已编译的框架（除了

sorry

）填充证明。

When to Use

适用场景

Proving theorems in Lean 4, from single lemmas to multi-file developments
Formalizing mathematics, protocols, or software specifications in Lean
Defining new types, structures, or functions in a Lean library
Reviewing Lean code for readability, maintainability, or Mathlib readiness
Refactoring a long or fragile tactic proof into lemmas
Setting up a formalization project that several people or agents will contribute to in parallel
Setting up CI, linters, or verification gates for a Lean project — do this at project start, before patterns propagate
Diagnosing slow proofs,
```
maxHeartbeats
```
timeouts, or expensive reduction
Writing custom tactics, macros, or project-specific linters

在Lean 4中证明定理，从单个引理到多文件开发项目
在Lean中形式化数学、协议或软件规范
在Lean库中定义新类型、结构或函数
审阅Lean代码的可读性、可维护性或是否符合Mathlib规范
将冗长或脆弱的策略证明重构为引理
搭建多人或多Agent并行贡献的形式化项目
为Lean项目搭建CI、检查器或验证关卡——在项目启动时就完成，避免不良模式扩散
诊断缓慢的证明、
```
maxHeartbeats
```
超时或高开销的归约问题
编写自定义策略、宏或项目专属检查器

When NOT to Use

不适用场景

Lean 4 as a general-purpose programming language (no proofs involved) — most of this skill targets proof and API structure
Coq, Isabelle, Agda, or Lean 3 — conventions and tactic names differ; Lean 3 idioms (
```
ge_or_gt
```
linting,
```
discrete_field
```
) are obsolete
Verified-software Lean projects with their own house style (e.g. spec-traceability-first codebases): Mathlib conventions are the community default, but check the project's CONTRIBUTING first and defer to it

将Lean 4作为通用编程语言（不涉及证明）——本技能的大部分内容针对证明和API结构
Coq、Isabelle、Agda或Lean 3——这些工具的规范和策略名称不同；Lean 3的惯用写法（如
```
ge_or_gt
```
检查、
```
discrete_field
```
）已过时
有自身内部风格的Lean验证软件项目（例如以规范可追溯性为首要目标的代码库）：Mathlib规范是社区默认标准，但请先查看项目的CONTRIBUTING文档并遵循其要求

The workflow

工作流程

1. Design definitions and their API first

1. 先设计定义及其API

Definitions carry the design weight. Before proving anything about a new concept:

Prefer total functions with junk values over subtypes or
```
Option
```
in signatures (Mathlib:
```
(0 : ℝ)⁻¹ = 0
```
). Side conditions then appear only on the lemmas that need them, not at every use site.
Bundle: new morphism kinds are structures with a
```
FunLike
```
instance; new subobject kinds use
```
SetLike
```
; carry property proofs as structure fields, not separate
```
IsHom
```
-style predicates.
Pick the canonical spelling (simp-normal form) for every concept with multiple equivalent forms, and state all API lemmas for that form only.
Write the API in the same file, immediately:
```
ext
```
,
```
@[simp]
```
, coercion, and injectivity lemmas — before the definition is used anywhere. Downstream proofs use the API, never
```
unfold
```
/
```
show ... from rfl
```
.

See library-design.md for the full set of design rules with rationale.

定义承载着设计的核心。在证明新概念的任何性质之前：

优先选择带无用值的全函数，而非签名中的子类型或
```
Option
```
（Mathlib示例：
```
(0 : ℝ)⁻¹ = 0
```
）。附带条件仅出现在需要它们的引理中，而非每个使用场景。
捆绑设计：新态射类型是带有
```
FunLike
```
实例的结构；新子对象类型使用
```
SetLike
```
；将属性证明作为结构字段，而非单独的
```
IsHom
```
式谓词。
选择标准写法（simp标准形式）：对于有多种等价形式的概念，选择一种标准写法，且所有API引理仅针对该形式陈述。
立即在同一文件中编写API：
```
ext
```
、
```
@[simp]
```
、强制转换和单射引理——在定义被任何地方使用之前完成。下游证明使用API，绝不使用
```
unfold
```
/
```
show ... from rfl
```
。

完整设计规则及原理请参考library-design.md。

2. Build a sorry skeleton

2. 构建sorry框架

State everything before proving anything, at every scale:

Project scale: state the target theorem and the lemmas it needs, all with
```
:= sorry
```
, and make the file compile. Each
```
sorry
```
is now an independent work unit — a contributor (human or LLM) can discharge one without understanding the rest. This is how LTE, PFR, and FLT scale to dozens of parallel contributors.
Proof scale: inside a proof, lay out the
```
have
```
/
```
suffices
```
/
```
calc
```
skeleton with
```
sorry
```
justifications, get Lean to accept the structure, then fill each step. Keeping the structure intact is what produces useful error messages while you work.

lean

example (a b c d : ℝ) (h : c = d * a + b) (h' : b = a * d) : c = 2 * a * d := by
  calc
    c = d * a + b     := sorry
    _ = d * a + a * d := sorry
    _ = 2 * a * d     := sorry

在证明任何内容之前，先完成所有层级的陈述：

项目层级：陈述目标定理及其所需的所有引理，全部使用
```
:= sorry
```
，并确保文件可编译。每个
```
sorry
```
现在都是独立的工作单元——贡献者（人类或LLM）无需理解其余部分即可完成其中一个。这就是LTE、PFR和FLT项目能扩展到数十位并行贡献者的方式。
证明层级：在证明内部，用
```
sorry
```
作为理由，搭建
```
have
```
/
```
suffices
```
/
```
calc
```
框架，让Lean接受该结构，然后填充每个步骤。保持结构完整能在工作时提供有用的错误信息。

lean

example (a b c d : ℝ) (h : c = d * a + b) (h' : b = a * d) : c = 2 * a * d := by
  calc
    c = d * a + b     := sorry
    _ = d * a + a * d := sorry
    _ = 2 * a * d     := sorry

3. Fill goals, one focused goal at a time

3. 逐个聚焦目标填充

Every new subgoal gets a focusing dot
```
·
```
with an indented block — never leave several goals active in unfocused sequence (Mathlib's
```
multiGoal
```
linter enforces this). This is what kills fragile goal-ordering dependence.
Open each block with a redundant
```
show
```
stating its goal. The proof works without it; reviewers and future editors need it. If
```
show
```
would change the goal, use
```
change
```
instead — keep stated goals honest.
Chained rewrites of (in)equalities become
```
calc
```
blocks, relations aligned vertically.
```
have
```
for forward stepping stones ("we first establish X");
```
suffices
```
for backward reduction ("it suffices to show X").
While drafting, annotate the goal state as a comment before non-obvious tactics — emitted by Lean, never imagined. In a headless workflow, insert
```
trace_state
```
at the point of interest or a deliberate
```
done
```
where goals should be closed, then run
```
lake env lean Path/To/File.lean
```
; copy the reported hypotheses, case name, and target. Strip routine probes after the proof works. This is the single most effective technique for LLM-written proofs (see llm-techniques.md).

See proof-style.md for the full tactic-style rules, and naming-conventions.md for naming lemmas so their names are guessable from their statements.

每个新子目标都要使用聚焦点
```
·
```
和缩进块——绝不要在未聚焦的序列中保留多个活跃目标（Mathlib的
```
multiGoal
```
检查器会强制执行此规则）。这能消除脆弱的目标顺序依赖问题。
每个块以冗余的
```
show
```
开头，陈述其目标。证明可以不依赖它，但审阅者和未来的编辑需要它。如果
```
show
```
会改变目标，请改用
```
change
```
——保持陈述的目标真实准确。
（不）等式的链式重写要变成
```
calc
```
块，关系要垂直对齐。
使用
```
have
```
进行正向推导（“我们首先确立X”）；使用
```
suffices
```
进行反向归约（“只需证明X即可”）。
起草时，在非显而易见的策略前添加注释标注目标状态——该状态由Lean生成，而非主观臆想。在无界面工作流中，在感兴趣的位置插入
```
trace_state
```
，或在目标应被关闭的位置故意插入
```
done
```
，然后运行
```
lake env lean Path/To/File.lean
```
；复制报告的假设、案例名称和目标。证明完成后移除常规探测代码。这是LLM编写证明最有效的技巧（请参考llm-techniques.md）。

完整策略风格规则请参考proof-style.md，引理命名规范请参考naming-conventions.md，以便从陈述中推测引理名称。

4. Verify mechanically

4. 机械验证

Do not eyeball-check style — run the checkers.

lake build

is the floor, and it is only the floor:

sorry

is a warning, so a green build exits 0 with sorries still present.

Gate unproved obligations by asking the kernel, never by grepping.
```
#print axioms myTheorem
```
for a spot check; for CI, collect axioms per declaration with
```
Lean.collectAxioms
```
and assert the whole expected footprint (
```
[propext, Classical.choice, Quot.sound]
```
unless deliberately widened), so a stray
```
sorry
```
or a new trust assumption like
```
native_decide
```
fails loudly. Grep is wrong in both directions: it matches the word in comments, and it misses a theorem whose own text is clean but which applies an unproved helper. Working script in linting.md.
Choose lints by project role and put them in CI at project start. Do not enable
```
linter.mathlibStandardSet
```
wholesale in a downstream project: it combines proof-maintenance checks with public-API checks, house style, and Mathlib-specific repository policy. For a self-contained proof, start with
```
linter.auxLemma
```
,
```
linter.style.maxHeartbeats
```
,
```
linter.style.multiGoal
```
,
```
linter.style.setOption
```
, and
```
linter.style.show
```
. A reusable library should additionally enable
```
linter.flexible
```
,
```
linter.style.missingEnd
```
,
```
linter.style.openClassical
```
, and the two
```
unused*InType
```
checks. Treat
```
nativeDecide
```
as a trust-policy choice and formatting or deprecated-syntax checks as project style. No warning gates anything unless warnings fail the build. Run Batteries' declaration-level
```
#lint
```
checks, including
```
simpNF
```
, separately. Verify every option against the pinned Mathlib source and with a known-trigger fixture: a misspelled
```
weak.
```
option is intentionally ignored. The complete 26-member audit and lakefile profiles are in linting.md.
Write a custom linter for every project-specific convention (simp-set discipline, summary-lemma coverage, required attributes) — a declaration-level
```
@[env_linter]
```
is one structure, and it is the only thing that reliably catches "the attribute is missing on 29 of 30 declarations". See linting.md for the recipe and the engineering rules (vacuity anchors, prove-it-can-fail, allowlists).

不要凭肉眼检查风格——运行检查工具。

lake build

是最低要求，且只是最低要求：

sorry

是警告，因此即使存在

sorry

，编译成功也会返回0。

通过内核而非 grep 检查未证明的义务。 使用
```
#print axioms myTheorem
```
进行抽查；在CI中，使用
```
Lean.collectAxioms
```
收集每个声明的公理，并断言整个预期的依赖范围（除非故意扩展，否则默认是
```
[propext, Classical.choice, Quot.sound]
```
），这样遗漏的
```
sorry
```
或新的信任假设（如
```
native_decide
```
）会触发明显失败。Grep在两个方向上都不可靠：它会匹配注释中的单词，也会遗漏自身代码干净但调用了未证明辅助定理的定理。可用脚本请参考linting.md。
根据项目角色选择检查器，并在项目启动时加入CI。 不要在下游项目中全盘启用
```
linter.mathlibStandardSet
```
：它结合了证明维护检查、公共API检查、内部风格和Mathlib专属仓库策略。对于独立的证明项目，从
```
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源码和已知触发用例验证每个选项：拼写错误的
```
weak.
```
选项会被故意忽略。完整的26项审计和lakefile配置请参考linting.md。
为每个项目专属规范编写自定义检查器（simp集合规则、摘要引理覆盖、必填属性）——声明级的
```
@[env_linter]
```
只需一个结构，且是唯一能可靠捕获“30个声明中有29个缺少属性”这类问题的方法。请参考linting.md中的实现方法和工程规则（空值锚点、证明可失败、白名单）。

The extraction ladder

提取阶梯

When does proof structure graduate into separate lemmas?

Before extracting, state the fragment's type and search by shape. Put the proposed statement in a scratch
```
example
```
, run
```
exact?
```
and
```
apply?
```
on the bare goal, then try a type-pattern and source search. If an existing theorem fits, use it. Do not report an API gap without recording the searches that failed.

A sub-argument repeats within one proof → name it as a local

have

lean

theorem min_comm (a b : ℝ) : min a b = min b a := by
  have h : ∀ x y : ℝ, min x y ≤ min y x := by
    intro x y
    apply le_min
    · show min x y ≤ y
      exact min_le_right x y
    · show min x y ≤ x
      exact min_le_left x y
  apply le_antisymm
  · show min a b ≤ min b a
    exact h a b
  · show min b a ≤ min a b
    exact h b a

The statement is independently interesting, or extraction sheds hypotheses the sub-argument does not need → standalone lemma. Dropping unneeded hypotheses is the stronger trigger: the extracted lemma becomes more general than the proof it came from.
The proof reads as "long and unwieldy" → split it. This is Mathlib's review criterion, and it is deliberately qualitative — there is no line threshold. Resolve doubt by attempting the extraction: if a fragment has a clean statement, it wanted to be a lemma.

何时将证明结构提炼为独立引理？

提取前，先陈述片段的类型并按形状搜索。 将拟议的陈述放入临时
```
example
```
中，对空目标运行
```
exact?
```
和
```
apply?
```
，然后尝试类型模式和源码搜索。如果已有合适的定理，请使用它。在报告API缺口前，务必记录已进行的搜索尝试。

子论证在单个证明中重复出现 → 将其命名为局部

have

。

lean

theorem min_comm (a b : ℝ) : min a b = min b a := by
  have h : ∀ x y : ℝ, min x y ≤ min y x := by
    intro x y
    apply le_min
    · show min x y ≤ y
      exact min_le_right x y
    · show min x y ≤ x
      exact min_le_left x y
  apply le_antisymm
  · show min a b ≤ min b a
    exact h a b
  · show min b a ≤ min a b
    exact h b a

陈述具有独立研究价值，或提取后能移除子论证不需要的假设 → 提炼为独立引理。移除不必要的假设是更强的触发条件：提炼后的引理会比它来源的证明更具通用性。
证明显得“冗长且难以处理” → 拆分它。这是Mathlib的审阅标准，且故意定性——没有行数阈值。通过尝试提取来解决疑问：如果片段有清晰的陈述，它就应该成为引理。

Quick reference

快速参考

Rule	Why	Enforced by
Never unfold definitions downstream; `erw` or trailing `rfl` = missing API	API lemmas are the abstraction boundary	review ("missing API" smell)
Terminal `simp` stays unsqueezed; non-terminal `simp` becomes `simp only [...]`	squeezed terminal calls bury the key lemmas and break on renames	style guide
One focused goal at a time ( `·` blocks)	kills goal-ordering fragility	`linter.style.multiGoal`
`show` must not change the goal (use `change` )	stated goals stay honest	`linter.style.show`
No `set_option` debug/trace/profiler or unscoped `maxHeartbeats` in final code	debugging scaffolding	`linter.style.setOption`
State lemmas in simp-normal form, `<` not `>`	simp matches syntactically	`simpNF` linter
Golf only when the result is at least as readable; trivial results exempt	short ≠ better	review
`Fact` instances are local, never global	global instances degrade all typeclass search	review
Name lemmas from their statements (see naming reference)	names become guessable without search	`linter.style.nameCheck` catches only `__` ; `#lint defsWithUnderscore` and review cover more
Search a bare goal by shape before writing a helper or claiming an API gap	names are not always guessable from the target	`exact?` , `apply?` , type/source search
Generally one tactic invocation per line; a one-line closing proof is the exception	preserves readable proof structure without inventing an absolute rule	style guide
Gate `sorry` with `collectAxioms` / `#print axioms` , never grep	grep matches comments, misses unproved helpers	axiom audit in CI
Prefer simp-lemma LHSs keyed on structure, not numerals; one spelling per constant	`2 ^ 32` never matches a goal normalized to `4294967296`	`simpNF` , review
Re-derive every `simp only` list with `simp?` at its own site	lists do not transfer between look-alike goals	`linter.flexible`
Every `maxHeartbeats` override is an unproven claim — measure before believing	copy-pasted budgets carry no information	`#count_heartbeats` , bisection
Conditional simp lemma fires shallow but not deep → raise `maxDischargeDepth` (default 2)	chained side conditions truncate silently, no diagnostic	diagnosis (proof-style, simp discipline)
Every project-specific convention gets a custom linter, in CI from day one	review misses the 29-of-30 failure mode	`@[env_linter]` + `#lint`

Full rationale for each row, plus the library-level anti-patterns, in anti-patterns.md.

规则	原因	强制执行方式
下游绝不展开定义； `erw` 或末尾 `rfl` 意味着缺少API	API引理是抽象边界	审阅（“缺少API”的不良气味）
末尾 `simp` 保持未压缩；非末尾 `simp` 改为 `simp only [...]`	压缩的末尾调用会隐藏关键引理，且在重命名时失效	风格指南
一次只聚焦一个目标（ `·` 块）	消除目标顺序的脆弱性	`linter.style.multiGoal`
`show` 不得改变目标（改用 `change` ）	保持陈述的目标真实准确	`linter.style.show`
最终代码中不得包含 `set_option` 调试/跟踪/分析器或未限定范围的 `maxHeartbeats`	移除调试脚手架	`linter.style.setOption`
引理陈述使用simp标准形式，用 `<` 而非 `>`	simp进行语法匹配	`simpNF` 检查器
仅当结果至少同样可读时才简化代码； trivial结果除外	短≠更好	审阅
`Fact` 实例是局部的，绝不是全局的	全局实例会降低所有类型类搜索的性能	审阅
根据陈述命名引理（请参考命名参考）	无需搜索即可推测名称	`linter.style.nameCheck` 仅捕获 `__` ； `#lint defsWithUnderscore` 和审阅覆盖更多情况
在编写辅助定理或声称API缺口前，先按形状搜索空目标	名称并非总能从目标中推测	`exact?` 、 `apply?` 、类型/源码搜索
通常每行一个策略调用；单行收尾证明是例外	在不制定绝对规则的前提下，保留可读的证明结构	风格指南
使用 `collectAxioms` / `#print axioms` 检查 `sorry` ，绝不使用grep	grep会匹配注释，遗漏未证明的辅助定理	CI中的公理审计
优先选择基于结构而非数字的simp引理左部；每个常量仅一种写法	`2 ^ 32` 永远无法匹配归一化为 `4294967296` 的目标	`simpNF` 、审阅
每个 `simp only` 列表都要在其所在位置用 `simp?` 重新生成	列表无法在相似目标间迁移	`linter.flexible`
每个 `maxHeartbeats` 覆盖都是未证实的断言——先测量再相信	复制粘贴的预算没有任何信息	`#count_heartbeats` 、二分法
条件simp引理浅层触发但深层不触发 → 提高 `maxDischargeDepth` （默认值为2）	链式附带条件会静默截断，无诊断信息	诊断（证明风格、simp规则）
每个项目专属规范都要有自定义检查器，从项目第一天就加入CI	审阅会遗漏“30个中有29个失败”的情况	`@[env_linter]` + `#lint`

每行规则的完整原理，以及库级别的反模式，请参考anti-patterns.md。

Rationalizations to reject

需摒弃的借口

Excuse	Reality
"The proof compiles, ship it"	Compiling is the floor. A monolithic tactic block that only Lean can read will break silently at the next Mathlib bump and no one will be able to repair it.
"Unfolding the definition is simpler than writing API lemmas"	Every downstream `unfold` couples a proof to the implementation. The first refactor breaks all of them at once. Write the missing lemma.
"Squeezing every simp makes the proof faster and more robust"	Backwards for terminal simp calls: the squeezed list breaks on every rename and drowns the signal. Squeeze non-terminal calls only.
"It's shorter, therefore better"	Mathlib review policy: golfing is fine only when it does not sacrifice readability. Length is not the target; legibility is.
"I'll restructure it into lemmas after it works"	After it works, the structure is load-bearing and tangled. State the skeleton first; the lemmas fall out for free.
"Adding `show` lines is redundant noise"	They are redundant to the kernel and essential to every human or model that reads the proof next.
"This helper is too specific to be a lemma"	If it has a clean statement, extract it — dropping the hypotheses it doesn't need usually reveals it was general all along.
"We'll add linters once the library stabilizes"	Backwards: patterns propagate by copy-paste, so a deferred linter meets a 400-warning backlog instead of one bad line. Enable what is already clean and gate it now.
"The check passed, so we're clean"	A check that can't fail proves nothing — sweeps reach zero files, misspelled `weak.` options are ignored, pipelines swallow exit codes. Prove every gate can fail before trusting that it passes.
"The proof is slow, raise maxHeartbeats"	An unmeasured budget is a claim, not a fix — and it masks the regression the next reader needs to see. Measure with `#count_heartbeats` ; restructure the definition or decompose the goal.

借口	真相
“证明能编译，直接发布”	能编译只是最低要求。只有Lean能读懂的单片策略块会在下次Mathlib更新时静默失效，且无人能修复。
“展开定义比编写API引理更简单”	每个下游 `unfold` 都会将证明与实现耦合。第一次重构就会一次性破坏所有相关证明。请编写缺失的引理。
“压缩每个simp能让证明更快更健壮”	对于末尾的simp调用来说，这是错误的：压缩后的列表会在每次重命名时失效，且掩盖关键信息。仅压缩非末尾调用。
“更短，因此更好”	Mathlib审阅政策：仅当不牺牲可读性时，简化代码才是可行的。长度不是目标；易读性才是。
“等证明完成后再重构为引理”	证明完成后，结构会成为支撑性的且相互缠绕。先陈述框架，引理会自然形成。
“添加 `show` 行是冗余的噪音”	对内核来说是冗余的，但对下一个阅读证明的人类或模型来说是必不可少的。
“这个辅助定理太特殊，不适合作为引理”	如果它有清晰的陈述，就提炼出来——移除它不需要的假设通常会发现它本来就具有通用性。
“等库稳定后再添加检查器”	恰恰相反：模式会通过复制粘贴传播，延迟添加检查器会遇到400条警告的积压，而非一条不良代码。现在就启用已符合规范的检查并设置关卡。
“检查通过了，所以我们没问题”	不会失败的检查毫无意义——扫描结果为零文件、拼写错误的 `weak.` 选项被忽略、流水线吞掉退出码。在信任检查通过前，先证明每个关卡都能失败。
“证明太慢，提高maxHeartbeats”	未测量的预算只是一种断言，而非修复——它会掩盖下一位读者需要看到的性能退化。用 `#count_heartbeats` 测量；重构定义或分解目标。

References

参考资料

library-design.md — definitions, APIs, bundling, abstraction boundaries, spec-driven project decomposition
proof-style.md — tactic proof structure: calc, have/suffices, focusing, and simp discipline including the why-doesn't-this-lemma-fire diagnoses (discharge depth, traversal order, numeral spellings)
naming-conventions.md — Mathlib naming so lemma names are computable from statements
anti-patterns.md — recognized anti-patterns, why each is harmful, and which linter catches it
llm-techniques.md — evidence-based techniques specific to LLM-written proofs
linting.md — axiom-based sorry gates, enabling project-specific linter profiles in CI early, the full Mathlib standard-set audit, adopting linters with a backlog, writing custom linters for project-specific constructs, and proving every gate can fail
performance.md — measuring per-declaration cost, where reduction cost comes from, optimizing definitions without losing semantics
tactics.md — metaprogramming discipline: extension-point selection, metavariable and recovery safeguards, bounded search, actionable errors, structured tracing, generated declarations, and failure-surface testing

library-design.md —— 定义、API、捆绑设计、抽象边界、基于规范的项目分解
proof-style.md —— 策略证明结构：calc、have/suffices、聚焦、simp规则，包括“为什么这个引理不触发”的诊断（释放深度、遍历顺序、数字写法）
naming-conventions.md —— Mathlib命名规范，让引理名称可从陈述中推导
anti-patterns.md —— 已识别的反模式、其危害及对应的检查器
llm-techniques.md —— 针对LLM编写证明的循证技巧
linting.md —— 基于公理的sorry关卡、尽早在CI中启用项目专属检查器配置、完整的Mathlib标准集审计、处理积压问题时采用检查器、为项目专属结构编写自定义检查器、证明每个关卡可失败
performance.md —— 测量单个声明的开销、归约成本的来源、在不丢失语义的前提下优化定义
tactics.md —— 元编程规则：扩展点选择、元变量和恢复保障、有界搜索、可操作的错误、结构化跟踪、生成的声明、故障表面测试

writing-lean-proofs

Original

Translation

Writing Lean Proofs

编写Lean证明

Contents

目录

When to Use

适用场景

When NOT to Use

不适用场景

The workflow

工作流程

1. Design definitions and their API first

1. 先设计定义及其API

2. Build a sorry skeleton

2. 构建sorry框架

3. Fill goals, one focused goal at a time

3. 逐个聚焦目标填充

4. Verify mechanically

4. 机械验证

The extraction ladder

提取阶梯

Quick reference

快速参考

Rationalizations to reject

需摒弃的借口

References

参考资料