图算法正确性的 Lean 4 机器检验：最大流–最小割定理形式化的构建与形式化工作量剖析

1 · 研究问题

在 Lean 4 与 mathlib 生态中，一名高中生能否在 12 个月内完成有限有向图上最大流–最小割定理（max-flow min-cut theorem）及 Ford–Fulkerson 方法在整数容量下终止性的、零 sorry 的机器检验证明？在这一过程中，纸笔证明里被视作"显然"的哪些步骤消耗了不成比例的形式化工作量（以证明行数、新增定义数、编译时间计），mathlib 的现有基础设施覆盖了其中多大比例？

2 · 研究背景与空白

技术背景。 交互式定理证明助手（interactive theorem prover）把数学证明写成机器可完全检查的形式对象：每一步推理都必须由内核逐条验证，任何跳步都会被拒绝。Lean 4 及其社区数学库 mathlib 是当前发展最快的体系，mathlib 已包含逾 11.5 万条定义与 23.2 万条定理，图论部分（SimpleGraph 及其配套）近年增长迅速，2025 年已有 Tutte 定理作为教学性形式化项目完成的公开记录，也有把超立方体最优 pebbling 数完整形式化的工作（20 个 Lean 源文件、约 12,071 行）。这类课题的算力特性极为特殊：它几乎不需要计算，只需要编译——Lean 的编译内存需求较高但完全在 16 GB 笔记本能力内，一台没有 GPU 的机器与一台服务器在形式化能力上没有差别。这是全部十条路线中"结构性绕开算力墙"最彻底的一条。

已有工作到哪一步。 mathlib 的图论部分已有匹配理论（Hall 婚配定理、Tutte 定理）等成果；形式化算法正确性（排序、树的插入删除）在 Lean 4 中被明确列为可行的应用方向；有面向 Lean 4 的综述（arXiv:2501.18639）与自动形式化基准工作。必须核实的关键事实：mathlib 当前是否已包含最大流–最小割定理或其等价形式（例如通过 Menger 定理或线性规划对偶）。 这一项无法凭记忆断定，必须在项目启动的头四周内用 mathlib 官方文档搜索与 loogle/Moogle 检索工具逐一确认，并以官方仓库当前状态为准。若已存在，整条路线必须立即换目标定理（见第 8 块降级路径）。

空白在于：形式化数学社区里"某定理是否已被形式化"有公开记录，但"形式化它花了多少代价、代价花在哪里"几乎没有系统的定量剖析；而这恰恰是决定形式化方法能否规模化的关键数据。本课题因此设计成双交付物：一份可编译的形式化，加一份形式化工作量剖析数据集。后者的价值不依赖前者是否完全完成——即使定理只形式化到一半，工作量剖析仍然成立。这一设计是本路线在高风险下仍可交付的根本保障。

3 · 可检验假设

• H1（工作量放大比）：完成的形式化的 Lean 代码行数与对应纸笔证明行数之比 ≥ 30 : 1，且其中 ≥ 60% 的行数消耗在纸笔证明中不显式出现的基础设施上（有限性论证、可判定性实例、图与流的表示转换、类型强制转换）。若比值 < 15 : 1，说明 mathlib 的覆盖已远超预期，这本身是对形式化成熟度的一次正面测量。
• H2（mathlib 覆盖率）：证明所需的引理中，能直接由 mathlib 现有定理满足的比例 ≥ 50%，而需自行证明的部分集中在"图上的归纳构造"这一类。若覆盖率 < 30%，则说明图算法方向的形式化基础设施仍然薄弱，本项目的中间引理本身具有向 mathlib 贡献的价值。

4 · 量化验收标准

1. 方法学校验（硬门槛）：在启动主定理之前，学生必须先独立完成一个已有公开形式化可供对照的小目标——例如插入排序的正确性与保序性、或 mathlib 中已有定理的一条独立重证——要求：lake build 通过、零 sorry、零 axiom（除 mathlib 标准公理外）、零 native_decide，并把自己的行数与结构同公开形式化对照，说明差异来源。这一步不过关（尤其是零 sorry 这一条），说明学生尚不具备完成主定理的能力，后续全部工作无效。"有 sorry 的证明不算证明"必须写死为项目纪律。
2. 主交付物的完成度判据：主定理的形式化按预先声明的引理清单逐条计分，每条引理有明确的"完成/未完成"二值状态（完成 = 零 sorry 且被主定理实际引用）。最终报告必须给出完整的引理清单与状态表，不得用"基本完成"这类表述。
3. 工作量剖析数据集（第二交付物，与主交付物同等重要）：对每条引理记录——Lean 行数、定义数、所用 mathlib 引理清单、首次编译通过前的提交次数、累计工时（学生自记，须每日记录而非事后回忆）、单独编译时间（中位数与 IQR，≥ 5 次重复）。这份数据集本身开源发布。
4. 统计口径：行数比与工时比是有界正量且分布高度偏斜，报中位数与 IQR，不报均值；覆盖率给 Clopper–Pearson 精确二项置信区间；分类（"基础设施" vs "核心论证"）须有预先写死的、可复现的判据，并由两人独立分类后报 Cohen's κ（κ < 0.6 则判据需重写）。
5. 可编译性与可复现性：整个项目作为一个 Lean 4 lake 包发布，锁定 mathlib 版本（lake-manifest.json 提交），提供在干净环境中的一键构建脚本与 CI 配置；第三方 clone 后 lake build 必须成功。
6. 诚实性条款：论文中出现的每一条形式化结论都必须对应仓库中一个零 sorry 的定理，并给出文件名与行号；任何未完成部分必须在正文中显式列出，不得省略。

5 · 数据与工具

用途	来源 / 工具
定理证明助手	Lean 4（leanprover/lean4，官方 elan 工具链管理器安装）+ mathlib4（社区数学库，通过 lake 依赖引入，版本须锁定）。纯 CPU，无 GPU 需求；mathlib 完整构建需数 GB 磁盘与较高编译内存，首次构建建议使用官方缓存 lake exe cache get 而非本地全量编译——这一点必须在第 1 周核实
定理检索	mathlib4 官方文档站（leanprover-community.github.io/mathlib4_docs）、loogle、Moogle、exact?/apply? 策略。用于核实"目标定理是否已存在"，这是本路线的头号前置任务
参照形式化	已公开的 Lean 4 教学性形式化项目（如 Tutte 定理形式化、超立方体 pebbling 形式化的 12,071 行代码）作为工作量对照点。仅用于校验与对比，不计入本项目贡献
纸笔证明底本	标准教科书证明（如 CLRS 的最大流最小割一节、Diestel《Graph Theory》），用于计算"纸笔行数"这一分母；底本须在正文指明版本与页码
备选目标定理	König 定理（二部图最大匹配 = 最小顶点覆盖）；Ford–Fulkerson 在整数容量下的终止性（独立于最大流最小割）；Dilworth 定理；Edmonds–Karp 的 O(VE²) 界。每一条都须先核实 mathlib 中是否已存在
工时与提交记录	Git 提交历史 + 学生每日工时表（模板固定，每日填写）
算力	纯 CPU。瓶颈是 Lean 编译的内存与时间：单文件编译通常秒级到分钟级，mathlib 缓存下载数 GB。16 GB 内存充裕。超出范围：任何需要大规模自动化证明搜索或训练模型的方案不在本课题范围内

6 · 方法路径

1. 装 elan + Lean 4 + mathlib（用官方缓存），跑通 mathlib 的示例与 lake build；建立项目骨架与 CI。
2. 核实目标定理的现状（本路线第一优先级、不可后延）：用官方文档、loogle、exact? 逐一检索最大流最小割及其等价形式、Menger 定理、线性规划对偶在 mathlib 中的状态，形成书面结论并附检索记录。结论决定主目标是保留还是切换。
3. 完成方法学校验（验收第 1 条）的小目标形式化，零 sorry 通过，并与公开形式化做行数与结构对照。
4. 把主定理拆成预先声明的引理清单（建议 15–30 条），为每条写出纸笔证明与 Lean 语句签名（theorem ... : ... := sorry），此清单在项目中期后不得再增删（增删须记录并说明理由）——这是使工作量剖析有意义的前提。
5. 自最基础的引理起逐条消去 sorry，每条完成即记录工作量剖析的全部字段；每周提交并保持 CI 绿。
6. 中期（第 26 周）盘点：按引理清单计分，判断主定理能否在剩余时间内完成，据此触发第 8 块的门槛决策。
7. 独立交叉校验与收尾：（a）请第三方（指导教师或社区）在干净环境中 clone 并 lake build，确认可复现；（b）对工作量分类做双人独立标注并报 κ；（c）把可复用的中间引理整理为向 mathlib 提交的候选（是否被接受不作为验收条件，但提交本身作为附录证据）。

7 · 新颖性边界

本课题不声称：不声称证明了任何新数学定理（最大流最小割定理是 1956 年的经典结果），不声称发明了新的证明方法，不开发新的证明助手或自动化策略，不涉及任何机器学习辅助证明。Lean 4、mathlib 与全部参照形式化均为他人工作，标注为对照基准，不计入本项目贡献。

已有工作完成了什么：mathlib 已含逾 11.5 万定义、23.2 万定理，图论部分已有 Hall 与 Tutte 等匹配理论成果，2025 年公开了 Tutte 定理的教学性形式化项目，另有超立方体最优 pebbling 数的完整 Lean 4 形式化（20 文件、12,071 行）；Lean 4 形式化算法正确性（排序、树操作）已被明确列为成熟应用方向。丘奖计算机赛道有两项高度相邻的历届获奖工作必须点名：2024 年金奖《LLM Mathematical Reasoning Grounded with Formal Verification》与 2023 年优胜奖《Close the Loop of Neural Intuition and Logical Reasoning for Geometry Theorem Proving》。两者的共同点是"用形式化工具为语言模型或神经直觉提供验证"，重心在 AI 一侧；本课题完全不涉及任何模型，重心在形式化工程本身与其工作量的定量剖析，方法与判断依据均不重叠。这一差异必须在论文引言中明确写出，否则极易被评委误认为同类。

本项目的贡献：（1）一份零 sorry 的、可被第三方一键复现的图论定理形式化（若 mathlib 中确不存在，则该形式化本身即为对公共基础设施的增量）；（2）一份形式化工作量剖析数据集——逐引理的行数、mathlib 依赖、工时与编译成本，以及"基础设施 vs 核心论证"的成本分解。第二项是主结论，也是本课题在主定理未能完成时仍然成立的保障。

为什么有价值：形式化数学的规模化瓶颈不在于"能不能形式化"，而在于"代价花在哪里"。逐引理的成本分解数据在公开文献中极为稀缺，而它直接指向"应该优先建设哪些基础设施"这一决策。

风险提示：若第 2 步核实发现 mathlib 已包含目标定理，本课题不因此失败——主目标切换到备选清单中的下一条，工作量剖析框架完全不变。这一点必须在方案里写死，因为它是本路线最可能触发的意外。

8 · 决策门槛（go / no-go）

• 第 4 周：目标定理现状核实完毕（不可后延）。若最大流最小割已在 mathlib 中，降级路径 A：按备选清单顺序切换目标（König 定理 → Ford–Fulkerson 整数终止性 → Dilworth 定理 → Edmonds–Karp 复杂度界），每次切换前同样先核实。工作量剖析框架与全部验收标准保持不变。
• 第 10 周：方法学校验硬门槛。若学生无法独立完成小目标形式化并零 sorry 通过，这是唯一一条应当整体放弃的门槛——本路线对形式化能力的要求无法通过投入时间弥补。此时立即整体改投 K03（同属离散/逻辑方向，SAT 编码课题对同类兴趣的学生适配度最高），已完成的 Lean 学习不浪费（SAT 与逻辑同源）。这一条必须提前告知学生与家长。
• 第 16 周：引理清单必须锁定，且已有 ≥ 20% 的引理零 sorry 完成。若完成比例 < 10%，降级路径 B：把主目标从"完整定理"缩为"该定理的一个受限版本"（例如限制在整数容量且图为有限简单有向图、或只形式化"最大流 ≤ 最小割"这一较易的方向），并把剩余方向明确列为未完成。主交付物缩水但工作量剖析完整。
• 第 26 周：中期盘点。若完成比例 < 50%，降级路径 C：正式把论文重心从"我们形式化了 X"转为"形式化 X 的工作量剖析与瓶颈识别"，主定理的未完成部分作为"已识别的瓶颈"写入结果而非隐去。这一降级保留了全部主结论框架，且在形式化社区中是被接受的贡献形态。
• 第 40 周：可复现性门槛。第三方干净环境 lake build 必须成功。若 mathlib 版本漂移导致构建失败，降级路径 D：把 mathlib 版本回退并锁定到最后一个可构建版本，在正文声明版本与日期。不得以"本地能跑"代替第三方复现。
• 预算裁剪顺序：向 mathlib 提交贡献（可完全砍掉）→ 引理清单规模（可缩至 15 条）→ 主定理的完整性（可缩为受限版本）→ （绝不裁剪）零 sorry 纪律、工作量剖析数据的每日记录、第三方可复现构建。
• 已知困难的定位：图上的归纳与有限性论证在 Lean 中的代价远高于纸笔，这是本课题预期中的主要成本来源——这个困难本身就是研究内容，应被测量并写入结果，而不是被当作障碍绕开。
• 选择前提：仅在学生已经自学过 Lean 或 Coq 的基础（能独立写出十几行的证明）、数学基础扎实、且明确接受"可能只完成一半定理"这一风险时才启动。这是全部十条路线中唯一一条对学生个人能力有硬性前置要求的路线；不满足前置条件时的正确做法是选 K03 而不是硬上。