附录 B — 形式化验证

建立经典李代数上幂零轨道闭包关系与分拆支配序间对应的原始论文 [1, section 3.2, p. 567] 在讨论 B、C、D 型合法分拆支配序的盖住关系时漏掉了几种情况，[2, proposition 3.9, theorem 3.10] 修补了这一漏洞．人类的注意力和耐心有限，在涉及大量繁琐分类讨论的情形下容易出现遗漏．鉴于此，我们对各型经典李代数合法分拆支配序的盖住关系（命题 2.2、命题 2.3 和命题 2.4）做了形式化验证．形式化的结果将在 Github 仓库开源¹．

¹ https://github.com/sun123zxy/nilpotent-orbit-classical-formalization．仓库未来可能更新，与本文发布时情况或存在差异．

我们选取的形式化验证工具是 Lean 4 证明助手 [3]，使用 mathlib4 数学库 [4], [5] 作为形式化验证的基础，相应 Lean 4 版本为 leanprover/lean4:v4.30.0-rc2．AI 工具方面，我们主要使用了 OpenAI 的 GPT 5.5 模型 [6] 和 Codex coding agent [7]．为使 coding agent 与 Lean 4 编译器正常交互，我们使用了 [8] 提供的 Lean LSP MCP 服务器，并编写了简单的 skill 文件指导 coding agent 进行 Lean 4 代码的编写和调试．

作为示例，下面我们重点介绍命题 2.2 和命题 2.3 的形式化经验．从环境配置完成到首次获得二者的完整形式化验证，整个过程历时两天，代码量约在 5000 行左右．成本方面，我们于 2026 年 5 月订阅了 OpenAI 售价 20 美元的 ChatGPT Plus 计划，整个形式化过程使用了约 60% 的周限额，若将订阅成本平均分配至各周，可认为成本在 3 美元左右．注意命题 2.4 的形式化和后续零散进行的整理和优化工作未计入成本统计．

B.1 人机协作流程

配置 Lean 4 项目环境，将论文草稿作为附件置入形式化项目，其中包括命题 2.2 和命题 2.3 的自然语言证明草案．使用 Codex 打开该形式化项目，告知其最终目标是完成命题 2.2 和命题 2.3 的形式化验证．
要求 Codex 首先阅读相关部分草稿并理解证明思路，检查草稿中是否存在明显的漏洞．如有，邀请其提供修正建议并手工修改．

Codex 在此过程中找到若干笔误和较小的逻辑漏洞，帮助完善了本文正文提供的证明．
要求 Codex 结合目标定理和证明，调查 mathlib4 相关基础设施建设情况，评估是否需要补充相关基础设施和形式化的难度．

我们选择命题 2.2 和命题 2.3 做形式化验证的一个重要原因是，它们的叙述都相对组合，无需大量李代数或代数几何的基础设施前置，成功实现形式化验证的可能性较大．Codex 的调查结果证实了这一点，其完成了 Nat.Partition、YoungDiagram 等相关定义定理现有状态的梳理．

证明过程经常需要取出分拆 \(\lambda\) 的从大到小排列的第 \(i\) 个部分 \(i \mapsto \lambda_i\)，且希望在超过长度的位置取值为 \(0\)．Nat.Partition 的实现是基于多重集 Multiset，后者是列表 List 商掉置换关系的结果．Codex 在调查后指出直接使用 Nat.Partition.parts 需要频繁处理排序和列表长度问题，不利于干净利落完成证明．为此其建议使用 YoungDiagram 作为主要基础设施，但这种方法可能涉及到构建限制 Young 图大小为定值的子类型，增加基础设施的复杂度．与 Codex 讨论后，我们最终决定增加 Nat.Partition 到 YoungDiagram 的转换函数 YoungDiagram.ofPartition，借助 Young 图侧已有的行长度函数 rowLen 为 Nat.Partition 定义 rowLen 和部分和函数 prefixSum，进而完成支配序 Dominates 的定义．这一设计为后续证明中使用 \(i \mapsto \lambda_i\) 提供了干净的接口．
要求 Codex 以实现 A 型分拆支配序盖住关系刻画命题 2.2 为目标，完成分拆支配序 Dominates 的定义，证明偏序关系并定义盖住关系的等价刻画．在过程中，我们提示 Codex 可以先用自然语言补全证明草案中省略的细节，确认无误后再进行形式化验证，如果发现证明草案有误时及时告知．

命题 2.2 的 \(\implies\) 侧声称 \(\lambda\) 盖住 \(\mu\) 时，存在位置 \(i,j\) 满足方块掉落条件．Codex 在此过程中意识到了方块掉落只是盖住关系的必要条件，并引入了 IsBoxDrop 和 IsCoverBoxDrop 两个新定义来区分普通方块掉落和对应盖住关系的方块掉落．最终，Codex 参考证明草案成功证明了比命题 2.2 的叙述更强的双向结果：
```
theorem isBoxDrop_of_covBy {n : ℕ} {mu lam : Nat.Partition n} (h : mu ⋖ lam) :
    IsBoxDrop lam mu := by sorry

theorem covBy_of_isCoverBoxDrop {n : ℕ} {mu lam : Nat.Partition n}
    (h : IsCoverBoxDrop lam mu) : mu ⋖ lam := by sorry

theorem covBy_iff_isCoverBoxDrop {n : ℕ} {mu lam : Nat.Partition n} :
    mu ⋖ lam ↔ IsCoverBoxDrop lam mu := by sorry
```
要求 Codex 整理 A 型分拆支配序盖住关系的证明，确认为此构建的基础设施可供后续 C 型分拆支配序盖住关系的证明使用；提前预测处理 C 型可能遇到的困难并讨论解决方案．

我们在此和 Codex 讨论确定了 C 型盖住关系的 API 设计，最终确定使用 Multiset 的计数函数 Nat.Partition.parts.count 定义条件 IsCPartition，并使用子类型定义 CPartition．在证明中，由于证明中经常使用 rowLens，因此我们先建立 Nat.Partition.count 和 YoungDiagram.rowLens.count 的一致性，从而在证明中主要使用 YoungDiagram.rowLen 风格的表述．

和之前 A 型的情况类似，我们引入了 IsCMove 来判断五种 C 型方块掉落，但不同于 A 型，我们未要求 Codex 额外证明命题 2.3 的 \(\impliedby\) 侧，故暂时没有引入 IsCoverCMove 来区分普通 C 型方块掉落和对应盖住关系的 C 型方块掉落．

要求 Codex 完成 C 型分拆支配序盖住关系命题 2.3 的形式化验证．

我们仍然引导 Codex 先用自然语言补全证明草案中省略的细节，确认无误后再进行形式化验证，并在发现证明草案有误时及时告知．Codex 发现了几处笔误，并给出命题 2.3 后评注中介绍的“一个不寻常的掉落”请求我们确认．此外，我们注意到 Codex 相当擅长提取和总结自然语言证明中重复出现的证明手段，例如其主动将分拆部分计数 YoungDiagram.rowLens.count 与一种被其称为 plateau 的 rowLen 函数区间的长度联系起来：

/-- Count a whole constant-height plateau in the row-length list. -/
lemma rowLens_count_eq_sub_of_plateau {N : ℕ} (p : Nat.Partition N)
    {a b m : ℕ}
    (hrow : ∀ r : ℕ, a ≤ r → r < b → p.rowLen r = m)
    (hprev : a = 0 ∨ m < p.rowLen (a - 1))
    (hnext : p.rowLen b < m) :
    ((YoungDiagram.ofPartition p).rowLens.count m) = b - a := by sorry

又例如，其识别出了自然语言证明中重复出现的 \(i_0, i, j\) 的格式，主动组织数据层级将其打包成 structure，从而简化了每个讨论中类似格式的证明的参数传递和证明结构：

/-- The first source row and first possible target row in a strict dominance interval. -/
structure FirstDropData {n : ℕ} (mu lam : Nat.Partition n) where
  i0 : ℕ
  j : ℕ
  hbefore : ∀ r : ℕ, r < i0 → mu.rowLen r = lam.rowLen r
  hstrict : mu.rowLen i0 < lam.rowLen i0
  hi0j : i0 < j
  hgap_i0 : lam.rowLen j + 1 < lam.rowLen i0
  hnoDrop : ∀ r : ℕ, i0 ≤ r → r < j → ¬lam.rowLen r + 1 < lam.rowLen i0
  hrowBefore : ∀ r : ℕ, r < j → mu.rowLen r ≤ lam.rowLen r

最终，Codex 形式化证明了如下结果：

theorem CPartition.isCMove_of_covBy {n : ℕ} {mu lam : CPartition n} (h : mu ⋖ lam) :
    IsCMove lam mu := by sorry

要求 Codex 整理证明、拆分文件、总结经验、提炼公共模式、遵守 Mathlib 编码规范并简化代码．

Codex 直出的代码倾向于使用大量 have 组织证明，导致代码冗长．我们引导 Codex 思考 A 型和 C 型证明中均出现过的类似模式，将相关数据打包成 structure，减少各定理的传参数量，避免冗余的数据打包解包，并在可能的情况行内化部分证明．面对我们的压行要求，Codex 没有直接盲目执行，而是调查后建议仅压缩不影响代码可读性的 have，使得代码没有因压行丧失可读性．此外，面对 Codex 直出代码中存在滥用 simp 和 omega 的情况，我们为其介绍了 Mathlib 此类定理的使用规范，引导其仅将 simp 用于终结证明并将 omega 替换为 ring、simp、rw 等更具体的工具．

B.2 Skill 文件

我们编写了一套简单的 skill 文件指导 Codex 进行 Lean 4 代码的编写和调试，除部分内容精简自 2026 年 1 月获取的 [9] 外，主要内容如下：

Mobilize lean-lsp-mcp if you have it in your tools. You can compile and run Lean code, access type information and error messages, etc. directly from MCP. Avoid using command line unless strictly necessary.
Always check diagnostic messages after your edit to ensure that your code is correct.
You may use Axiom of Choice, functional extensionality, propositional extensionality, quotient axioms, and noncomputable in your code. But if it permits, minimize their usage.
Cheating is not allowed. Adding new axioms are strictly prohibited. You may only use sorry to temporarily bypass a proof obligation, but you should eventually fill in the proof. Only sorry if you tried really hard but failed. In such a case, report where you got stuck, what you have tried, and possible next steps for the user’s consideration.
Do not use rw-like tactics for definitions. This tends to give very bad definitional equality and is strictly prohibited in Mathlib.
Respect the 100 character limit per line.

B.3 其它 AI 工具的尝试

我们也对部分其它 LLM 和 coding agent 做了尝试，例如配备 Gemini 3.1 Pro、Claude 4.6 Sonnet 和 Deepseek v4 Pro 的 Github Copilot．其中，Deepseek v4 Pro 在处理 Lean 4 代码时表现较差，往往在较长时间的思考和全盘推翻重构间徘徊不前；Claude 4.6 Sonnet 在处理 Lean 4 代码时消耗大量 token 思考未做行动，经常超出 Github Copilot 的最大回复 token 限额，我们推测这是二者之间 agent harness 不甚良好所致，在 Claude Code 中使用或会有更好的表现；Gemini 3.1 Pro 在我们的测试中表现优于前两者，能够在多次修正后完成命题 2.2 部分基础设施的建设，但其写出的 Lean 4 代码时常无法一次性通过编译，往往需要多次编译器反馈才能修正，效率和质量都不及预期．

B.4 总结

函数式编程的优势之一在于丰富的编译器反馈，这对 coding agent 来说是宝贵的资源．总的来说，在目前的 AI 技术水平下，使用 Codex coding agent 配合 Lean LSP MCP 服务器进行 Lean 4 代码的编写和调试是完成数学形式化验证的可行方案，且效率和质量都相对理想；使用其它 LLM 和 coding agent 则需注意二者的适配情况，确保使用优质模型搭配良好的 agent harness．部分头部开源模型相较头部闭源模型在数学形式化验证任务方面还有一定差距，目前难以胜任中等复杂度的形式化验证任务．

[1]

M. Gerstenhaber, 《Dominance Over The Classical Groups》, Annals of Mathematics, 卷 74, 期 3, 页 532～569, 1961, doi: 10.2307/1970297.

[2]

W. Hesselink, 《Singularities in the nilpotent scheme of a classical group》, Transactions of the american mathematical society, 卷 222, 页 1～32, 1976, 见于: 2026年4月28日. [在线]. 载于: https://www.ams.org/tran/1976-222-00/S0002-9947-1976-0429875-8/

[3]

L. de Moura 和 S. Ullrich, 《The Lean 4 Theorem Prover and Programming Language》, 收入 Automated Deduction – CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings, Berlin, Heidelberg: Springer-Verlag, 2021, 页 625～635. doi: 10.1007/978-3-030-79876-5_37.

[4]

The mathlib Community, 《The Lean Mathematical Library》, 收入 Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 收入 CPP 2020. New Orleans, LA, USA: ACM, 1月 2020. doi: 10.1145/3372885.3373824.

[5]

A. Baanen, M. R. Ballard, J. Commelin, B. G. Chen, M. Rothgang, 和 D. Testa, 《Growing Mathlib: maintenance of a large scale mathematical library》. arXiv, 2025年8月29日. doi: 10.48550/arXiv.2508.21593.

[6]

OpenAI, 《Introducing GPT-5.5》. 2026年. 见于: 2026年5月26日. [在线]. 载于: https://openai.com/index/introducing-gpt-5-5/

[7]

OpenAI, 《Introducing Codex》. 2025年. 见于: 2025年5月26日. [在线]. 载于: https://openai.com/index/introducing-codex/

[8]

O. Dressler, 《Lean LSP MCP: Tools for agentic interaction with the Lean theorem prover》. 2025年3月. 载于: https://github.com/oOo0oOo/lean-lsp-mcp

[9]

C. Freer, 《Lean 4 Skills: Theorem proving skill and workflow pack for AI coding agents》. 2025年10月. 载于: https://github.com/cameronfreer/lean4-skills