读完这篇你能拿到三个具体产物：一个装了 mathlib 的 Lean 4 工程；一个"命题被冻结、只让模型填证明"的半自动回路；一份 sorry 审计报告，能明确告诉你哪些定理是真证出来的、哪些还挂着洞。整个流程在一个下午能跑通，产出是一个陈述 100% 编译通过、证明还剩若干个 sorry 的文件——这本身就是有价值的中间成果，因为形式化领域公认最难的一半是"把猜想写对"，不是"把证明写完"。
先把心智模型立住，后面所有操作都围绕它：
> Lean 验证的是"你给出的证明项，确实证明了你自己写的那个命题"。它不验证命题是否为真，也不验证命题是不是你心里想的那个。
所以"编译通过"和"猜想成立"是两件事。把这两件事分开，你才不会被 LLM 骗。
前置条件清单
动手前确认这些就位：
- 一台能装 Linux/macOS 的机器，Node 与 Python 3 环境；
- 磁盘预留若干 GB（mathlib 的源码加预编译缓存体积不小，具体以官方仓库说明为准）；
- 编辑器用 VS Code + Lean 4 官方扩展，能实时看到 goal 状态——这一步体验提升巨大，别省；
- 一个能通过 API 调用的 LLM（本地部署也行），要求能接受长文本输入并稳定输出代码；
- 命令行基础：
cd、grep、export。
不需要你懂 Lean 的证明策略细节。需要你有耐心看编译器报错。
第一步：装工具链，跑通"Hello World"
Lean 4 的标准做法是用 elan 管理工具链版本，用 lake 做构建。安装脚本地址以 Lean 官方页面为准，这里用占位符表示：
```bash
安装脚本的准确 URL 以 Lean 官方文档为准
curl -sSf <官方 elan 安装脚本 URL> | sh
source ~/.profile
elan --version
elan toolchain list
```
然后建一个依赖 mathlib 的工程：
```bash
模板名与参数以 lake 官方文档为准
lake new ns_demo math
cd ns_demo
lake update
lake exe cache get # 拉取 mathlib 预编译缓存，强烈建议先做这步
lake build
```
lake exe cache get 是关键。没有它，第一次编译 mathlib 会等到你怀疑人生。
验证环境：
```lean
import Mathlib
example (a b : ℕ) : a + b = b + a := by
exact Nat.add_comm a b
```
把这段存成 Scratch.lean，用 lake env lean Scratch.lean 单独跑。试验文件用 lake env lean，正式定理放进库目录再 lake build，这样编译速度快很多。
第二步：把猜想写成"冻结的命题"
这一节是整篇文章最重要的部分。
假设你想碰 Navier–Stokes 方向。三维 Navier–Stokes 全局正则性这种级别的问题，完整形式化是多年工程（社区里已有 PDE 形式化的持续努力，具体进展以官方仓库为准），不适合作为第一天的目标。正确做法是分层降级：先形式化一个真实但小得多的能量不等式玩具模型，把流水线跑通。
```lean
import Mathlib
set_option autoImplicit false
/-- 玩具模型：一维标量版本的"能量衰减"。
真实 NS 能量估计是 ‖u(t)‖² + 2ν∫₀ᵗ‖∇u‖² ≤ ‖u(0)‖²，
这里先砍掉空间维度与梯度项，只留下"耗散让能量不增"的骨架。 -/
theorem toy_energy_decay
(ν : ℝ) (hν : 0 < ν) (u : ℝ → ℝ)
(h : ∀ t, 0 ≤ t → HasDerivAt u (-(ν * u t)) t) :
∀ t, 0 ≤ t → (u t) ^ 2 ≤ (u 0) ^ 2 := by
sorry
```
再看离散几何方向。Erdős–Szekeres 是这块的经典热点，二维"凸位置"版本需要 orientation、凸包等一大堆几何定义，同样先降级到一维单调子序列版本：
```lean
/-- 一维 Erdős–Szekeres：长度 (r-1)(s-1)+1 的互异实数序列，
必有长度 r 的递增子序列或长度 s 的递减子序列。 -/
theorem erdos_szekeres_one_dim
{n r s : ℕ} (hr : 0 < r) (hs : 0 < s)
(hn : (r - 1) * (s - 1) + 1 ≤ n)
(a : Fin n → ℝ) (hinj : Function.Injective a) :
(∃ f : Fin r → Fin n, StrictMono f ∧ StrictMono (a ∘ f)) ∨
(∃ g : Fin s → Fin n, StrictMono g ∧ StrictAnti (a ∘ g)) := by
sorry
```
现在关键技巧来了：别把命题写在 theorem 的签名里。把它抽成一个 def，让命题变成不可篡改的常量：
```lean
def Conjecture_ES1D : Prop :=
∀ {n r s : ℕ}, 0 < r → 0 < s → (r - 1) * (s - 1) + 1 ≤ n →
∀ (a : Fin n → ℝ), Function.Injective a →
(∃ f : Fin r → Fin n, StrictMono f ∧ StrictMono (a ∘ f)) ∨
(∃ g : Fin s → Fin n, StrictMono g ∧ StrictAnti (a ∘ g))
theorem es_1d : Conjecture_ES1D := by
sorry
```
为什么要这样？因为 LLM 最容易犯的错，不是证不出来，而是偷偷把命题改弱——把 < 换成 ≤、悄悄加一个前提、把量词顺序调一下。一旦命题被抽成 def Conjecture_ES1D，模型无论怎么改证明体，都不可能改到命题本身。它要是想改，只能去改 def，那你一眼就能看见。
顺带一句：def 定义 Prop 不需要证明，所以这段代码本身就能编译通过。sorry 也不是错误，只是警告——这是 Lean 的设计意图，但对 CI 是灾难，后面必须审计。
第三步：让 LLM 只填证明，不碰陈述
写一个 Python 回路：读文件 → 编译 → 把错误喂回模型 → 让模型只输出证明体 → 校验命题指纹没变 → 写回 → 再编译。
```python
import subprocess, pathlib, re, hashlib
ROOT = pathlib.Path(".").resolve()
TARGET = ROOT / "NsDemo" / "Target.lean"
def run_lean(timeout=600):
"""单独编译一个试验文件，比 lake build 快。"""
p = subprocess.run(
["lake", "env", "lean", str(TARGET)],
cwd=ROOT, capture_output=True, text=True, timeout=timeout,
)
return p.returncode, (p.stdout + p.stderr)
def count_sorry(text: str) -> int:
粗略计数，正式审计用 #print axioms
return len(re.findall(r"\bsorry\b", text))
def statement_of(text: str) -> str:
"""取 := 之前的部分当作命题指纹，防止模型悄悄改陈述。"""
return text.split(":=")[0].strip()
def fingerprint(text: str) -> str:
return hashlib.sha256(statement_of(text).encode()).hexdigest()[:12]
def extract_lean(reply: str) -> str:
m = re.search(r"``lean\s*(.*?)``", reply, re.S)
return (m.group(1) if m else reply).strip()
PROMPT = """你是一个 Lean 4 / mathlib 证明助手。
【硬性约束】
1. 只允许修改定理的证明体（by 后面的部分）。
2. 绝对不允许修改定理名、参数、假设、结论，一个字都不许动。
3. 不允许新增 axiom，不允许用 sorry 之外的占位。
4. 如果一步证不完，就输出多个子引理，每个子引理体用 sorry，
并在注释里写清楚这个子引理打算怎么证。
【当前文件】
{code}
【编译器输出】
{errors}
只输出一个 ```lean 代码块，里面是完整的、可直接落盘的文件内容。"""
这里接你自己的模型 SDK；以你所用服务的官方文档为准
def ask_llm(prompt: str) -> str:
raise NotImplementedError("接入你用的模型客户端")
def solve(max_rounds: int = 12):
base_fp = fingerprint(TARGET.read_text())
for i in range(max_rounds):
code = TARGET.read_text()
rc, err = run_lean()
n_sorry = count_sorry(code)
print(f"[round {i}] rc={rc} sorry={n_sorry}")
if rc == 0 and n_sorry == 0:
print("没有 sorry 且编译通过，进入人工复核。")
return True
reply = ask_llm(PROMPT.format(code=code, errors=err[-6000:]))
new_code = extract_lean(reply)
if fingerprint(new_code) != base_fp:
print("!! 检测到命题被修改，拒绝写回。")
continue
TARGET.write_text(new_code + "\n")
return False
if __name__ == "__main__":
solve()
```
几个细节值得强调：
- 错误只截取尾部若干字符喂回去，不要贴整个编译日志，否则上下文立刻爆掉；
- 第一次迭代几乎必然会报错，这很正常，报错本身是最有价值的信号；
- 每次写回前校验指纹——这一步能挡掉绝大多数"模型自作聪明"事故。
第四步：用 #print axioms 做 sorry 审计
grep sorry 只看字面量，模型把漏洞藏进一个中间引理时你就漏了。真正的审计手段是 #print axioms：
```lean
-- 放在文件末尾
#print axioms es_1d
#print axioms toy_energy_decay
```
编译时 Lean 会打印这个定理依赖的公理清单。正常情况下你会看到 propext、Classical.choice、Quot.sound 这三条 mathlib 标准公理；一旦出现 sorryAx，说明证明里还有洞。这一步是"可验证"三个字的落点，务必写进 CI。
```bash
简易守门脚本：出现 sorryAx 就退出非零
lake env lean NsDemo/Target.lean | grep -q "sorryAx" && echo "存在未完成证明" && exit 1
```
常见坑与排错
把 sorry 当成"证完了"。 sorry 会让文件编译通过，CI 会绿。必须靠 #print axioms 兜底。
模型偷偷改弱命题。 前面 def Conjecture + 指纹校验就是治这个的。再加一道保险：另写一个 example : Conjecture_ES1D := es_1d，如果命题被改过，这行会直接报类型不匹配。
幻觉引理名。 模型会一本正经地写出不存在的 Mathlib.Foo.bar_lemma。不要跟它争，直接在文件里加 #check 那个名字，编译一次就知道真假。更好的办法是让 Lean 自己找：exact?、apply?、simp? 这类搜索式 tactic 会用当前 goal 去检索 mathlib，比模型猜准得多。
隐式变量带来的诡异错误。 在文件开头写 set_option autoImplicit false。否则模型打错的变量名会被 Lean 当成隐式自由变量默默接受，最后给你一个莫名其妙的类型错误。
版本漂移。 toolchain 和 mathlib 必须一起更新，具体版本约束以工程的 lakefile 为准。别手动改 toolchain 文件，用 elan 和 lake update。
大定理一步到位。 让模型一次证完 Erdős–Szekeres 是不现实的。正确姿势是让它先吐 3 到 5 个子引理的签名，每个都用 sorry，然后再逐个攻破。这一步"先规划后证明"的效果，比反复重试同一目标好得多。
超时与 tactic 爆炸。 复杂的 simp 会跑很久。可以临时 set_option maxHeartbeats 400000 抬高上限，但更该做的是把目标拆小。
上下文塞太多。 别把整个 mathlib 源码喂进去。给签名、给报错、给几条 #check 结果就够了。
下一步建议
先练陈述，再练证明。 把形式化工作量按 7:3 分配——七成时间花在把猜想精确地写成 Prop，三成给证明。你可以专门做一个"只写陈述、全部 sorry"的文件集合当 benchmark，这个练习对判断模型能力上限非常有用。
引入自动化 tactic 打底。 omega 管线性整数算术，linarith/nlinarith 管线性与多项式不等式，positivity 管正性，gcongr 管不等式链，aesop 做通用搜索。让模型先试这些，失败再写手工证明，成功率会明显提升。
从一维走向二维。 一维 Erdős–Szekeres 跑通后，二维版本的增量工作主要是定义"一般位置""凸位置"这类几何谓词，然后证明一维结论能提升上去。这条路径比直接冲三维 Navier–Stokes 现实得多。
把 sorry 数量做成指标。 每次提交记录剩余 sorry 数，只允许下降不允许上升。这个朴素规则比任何"证明质量评估"都管用。
人永远保留最后一道关。 LLM 负责生成证明草稿、搜索引理、搬运繁琐代数；你负责把命题写对、判断这个定理值不值得证、以及审查最终 #print axioms 的干净程度。这个分工在可预见的未来都不会变。
跨领域迁移。 这套"冻结命题 → 编译 → 报错回喂 → 审计公理"的回路，和领域无关。换成图论、组合优化、密码学协议的安全性证明，流程完全一样。真正的门槛从来不是 Lean 的语法，是你有没有能力把一句中文的数学直觉，翻译成一个编译器能接受的、不多不少刚刚好的 Prop。