Duality theory in linear optimization and its extensions -- formally verified

本文在 Lean 4 中形式化证明了线性有序域上的多个 Farkas 型定理，并将对偶理论扩展至允许系数取“无穷大”的情形。

要点

这篇论文就像是一份**“数学世界的法律条文验证报告”**。

想象一下，你是一位**“数学法官”，而这篇论文的作者（Martin Dvorak 和 Vladimir Kolmogorov）是两位严谨的“法律起草者”。他们的工作不是发明新法律，而是用一种叫 Lean 4 的“超级严谨的计算机语言”，把关于线性规划（Linear Optimization）的一些古老法律条文重新写了一遍，并让计算机逐字逐句地检查**，确保这些法律在任何情况下都绝对正确，没有任何逻辑漏洞。

下面我用几个生活中的比喻来拆解这篇论文的核心内容：

1. 核心故事：寻找“不可能”的真相（Farkas 引理）

背景故事：
想象你在经营一家餐厅，有一堆食谱（线性不等式）。你想知道：“有没有一种食材搭配方案，能同时满足所有食谱的要求？”

Farkas 引理（Farkas' Lemma）告诉我们：
在这个世界里，只有两种情况，非此即彼：

1. 有解： 真的存在一种食材搭配，能完美满足所有要求。
2. 无解： 根本不存在这种搭配。但是，如果你把食谱里的要求混合在一起（比如把“盐要少”和“盐要多”加起来），你会得到一个荒谬的结论（比如"0 < 0"，即“没有盐比有盐还多”）。

论文做了什么？
作者说：“以前数学家们凭直觉相信这个定理是对的。但我们用计算机（Lean 4）把证明过程像搭积木一样，一块一块地拼起来，100% 确认这个定理在数学上是无懈可击的。”

2. 新突破：引入“无限大”的魔法（扩展实数）

这是这篇论文最酷的地方。

传统困境：
在传统的数学世界里，数字是有边界的。但在现实生活中，有些约束是**“硬性”的，有些是“软性”**的。

• 例子（廉价午餐）： 你想做一顿饭，要求至少 30 克蛋白质，至少 700 卡路里。
  • 软约束： 尽量便宜（这是目标）。
  • 硬约束： 必须满足营养（这是底线）。

如果某种食材（比如扁豆）没货了，传统数学怎么处理？

• 笨办法： 把扁豆的价格设为"999999 欧元”。但这很尴尬，因为如果预算是 100 万，这个价格就失效了。而且，如果没货，为什么还要在公式里留个位置？
• 作者的魔法： 直接给没货的食材价格贴上**“无穷大” ($\infty$)** 的标签！

论文的贡献：
作者把数学理论扩展到了**“带无穷大的世界”**。

• 他们定义了一套新规则：如果某个东西是“无穷大”，那它比任何有限数字都大。
• 他们还处理了**“负无穷大”**（比如某种东西不仅没货，而且如果你敢用，世界就会毁灭）。
• 关键点： 他们证明了，即使在这个充满“无穷大”的混乱世界里，那个“有解或无解”的定理依然成立！只要小心处理“正无穷”和“负无穷”不能在同一行打架的规则。

比喻：
这就好比你在玩一个游戏，以前只能选“苹果”或“梨”。现在游戏允许你选“苹果”、“梨”或者**“整个宇宙”**（无穷大）。作者写了一本新指南，告诉你：即使你选了“整个宇宙”，游戏的胜负规则（对偶理论）依然清晰有效。

3. 对偶理论：看问题的两面性

论文还验证了**“强对偶定理”**。

• 比喻： 想象你在玩一个**“零和博弈”**游戏。
  • 玩家 A（原始问题）： 想最小化成本（比如买午餐）。
  • 玩家 B（对偶问题）： 想最大化某种“影子价格”（比如蛋白质的价值）。
• 定理说： 如果游戏是公平的（有解），那么玩家 A 能达到的最低成本，正好等于玩家 B 能达到的最高价值。
• 作者的工作： 他们证明了，即使在这个允许“无穷大”价格的新游戏里，只要规则设定得当（Valid ELP），这个“收支平衡”的奇迹依然会发生。

4. 为什么这很重要？（Lean 4 的作用）

你可能会问：“数学家证明这些不就行了吗？为什么要用计算机？”

• 人类会犯错： 人类在推导几百步的复杂逻辑时，可能会漏掉一个微小的假设（比如“这里不能是负数”）。
• 计算机不撒谎： Lean 4 就像一个**“强迫症级别的校对员”**。它不关心直觉，只关心逻辑链条是否严丝合缝。如果有一步推导不成立，它会直接报错，绝不通过。
• 结果： 这篇论文不仅仅是“证明了一个定理”，而是**“为线性优化领域建立了一套绝对可信的数字基石”**。未来的工程师、AI 算法开发者，如果用到这些理论，可以确信背后的数学逻辑是坚不可摧的。

总结

这篇论文就像是在数学的摩天大楼里，用激光扫描仪（Lean 4）重新检查了地基和承重墙。

1. 确认了旧地基： 经典的线性规划定理（Farkas 引理）在普通数字世界里是绝对稳固的。
2. 扩建了新楼层： 他们成功地把大楼扩建到了**“无穷大”**的领域，并证明了即使面对“无穷大”这种极端情况，大楼的结构依然安全，不会倒塌。

对于普通人来说，这意味着：当我们用计算机去优化物流、调度资源或设计 AI 时，背后的数学逻辑比以往任何时候都更加可靠和强大。

技术摘要

这是一篇关于线性优化对偶理论及其扩展的形式化验证论文，发表于《形式化数学年鉴》（Annals of Formalized Mathematics）。作者 Martin Dvorak 和 Vladimir Kolmogorov 使用 Lean 4 证明语言和 Mathlib 库，在形式化数学领域取得了重要进展。

以下是对该论文的详细技术总结：

1. 研究问题 (Problem)

线性规划（Linear Programming, LP）的核心在于对偶理论，特别是 Farkas 引理（Farkas Lemma）和 强对偶定理（Strong Duality Theorem）。这些定理建立了线性不等式系统的可解性与线性组合矛盾之间的等价关系。

然而，现有的形式化工作（如在 Isabelle 或 Rocq 中）主要关注标准实数或有理数域上的线性规划。在实际应用中（如离散优化中的“硬”约束），往往需要处理无限大系数（例如，将某些变量设为无穷大以强制满足约束）。传统的线性规划理论无法直接处理包含 $\infty$（正无穷）和 $-\infty$（负无穷）的扩展实数域，因为标准的算术运算（如 $0 \cdot \infty$或$\infty + (-\infty)$）在这些情况下会导致定义模糊或逻辑矛盾。

核心问题：

1. 如何在更一般的代数结构（如线性有序除环）上形式化 Farkas 引理？
2. 如何构建一个包含无限值的扩展线性有序域（Extended Linearly Ordered Field），并在此框架下形式化线性规划的对偶理论？
3. 在引入无限值后，如何定义线性规划的可行性、无界性和最优解，并证明强对偶定理依然成立？

2. 方法论 (Methodology)

作者完全使用 Lean 4 及其数学库 Mathlib 进行形式化证明。

• 代数基础构建：

  • 利用 Mathlib 现有的代数层级（Algebraic Hierarchy），从半群、环、域逐步构建到线性有序除环（Linearly Ordered Division Ring）。
  • 由于 Mathlib 原生未包含“线性有序除环”类，作者自定义了该类，并建立了其与线性有序域之间的实例转换，以支持非交换乘法场景下的 Farkas 引理推广。
  • 定义了模（Module）和线性映射，特别是处理了标量乘法与偏序之间的单调性关系（PosSMulMono）。

• 扩展域的定义：

  • 定义了扩展线性有序域 $F_\infty = F \cup \{-\infty, +\infty\}$。
  • 重新定义了加法、取反和标量乘法。特别地，作者采用了特定的算术规则：$-\infty + \infty = -\infty$ 和 $0 \cdot (-\infty) = -\infty$。这使得$F_\infty$ 不再是域或群，而是一个稠密线性有序阿贝尔幺半群。
  • 定义了矩阵与向量的乘法，特别是处理了非标准维度和混合类型（有限值与无限值）的乘法（dotWeig 和 Matrix.mulWeig）。

• 形式化策略：

  • 归纳法证明：在证明 Bartl 推广的 Farkas 引理时，使用了基于有限类型大小的归纳法。
  • 构造性证明：通过构造对偶变量或原问题解来证明“二者必居其一”（Theorems of Alternatives）。
  • 反例验证：对于扩展理论中的六个必要条件，作者不仅证明了其必要性，还通过构造具体的反例（Counterexamples）来展示若缺少任一条件，定理将不再成立。

3. 关键贡献 (Key Contributions)

A. 广义 Farkas 引理的形式化

作者形式化并证明了 Bartl 提出的更通用的 Farkas 引理版本：

• 非交换性：支持线性有序除环（乘法不一定交换）。
• 无限方程：支持无限多个方程（通过线性映射定义）。
• 一般模结构：将向量空间推广到一般的 $R$-模 $W$ 和线性有序 $R$-模 $V$。
• 定理 1.6 (fintypeFarkasBartl)：这是最通用的形式，涵盖了之前所有的 Farkas 类型定理。

B. 扩展线性规划理论 (Extended Linear Programming)

这是本文最具创新性的部分，将线性规划推广到包含无限值的场景：

• 定义扩展线性规划：允许矩阵 $A$、向量 $b$ 和 $c$ 中包含 $\infty$ 和 $-\infty$。
• 定义“有效”线性规划 (Valid ELP)：为了确保对偶定理成立，定义了六个严格的预处理条件（例如：同一行不能同时包含 $\infty$ 和 $-\infty$；若 $b$ 为 $\infty$，则 $A$ 对应行不能有 $\infty$ 等）。
• 扩展 Farkas 引理 (Theorem 1.8)：证明了在满足上述条件下，扩展线性不等式系统的可解性与对偶矛盾的存在性是互斥且完备的。
• 扩展强对偶定理 (Theorem 1.11)：证明了对于有效的扩展线性规划，原问题最优值 $P^*$ 与对偶问题最优值 $D^*$ 满足 $P^* = -D^*$（在扩展实数意义下）。

C. 形式化基础设施

• 构建了处理扩展实数运算的专用库，特别是处理 $0 \cdot \infty$ 等边界情况。
• 重新定义了矩阵与向量的乘法算子，以支持非标准类型（如 $F_\infty$ 与 $F_{\ge 0}$ 的混合运算）。

4. 主要结果 (Results)

1. 定理 1.1 - 1.3 (标准形式)：在 Lean 中重新证明了经典的等式/不等式 Farkas 引理和标准线性规划强对偶定理。
2. 定理 1.4 - 1.6 (Bartl 推广)：成功形式化了 Bartl 关于非交换环和一般模的 Farkas 引理推广，这是此前未形式化的成果。
3. 定理 1.8 (扩展 Farkas)：证明了在 $F_\infty$ 上，只要满足四个关于 $\infty$ 和 $-\infty$ 分布的约束条件，Farkas 引理依然成立。
4. 定理 1.11 (ValidELP.strongDuality)：证明了在满足六个“有效性”条件的扩展线性规划中，强对偶定理成立。
   • 如果原问题可行且对偶可行，则 $P^* = -D^*$。
   • 如果原问题可行但对偶不可行，则原问题无界（$P^* = -\infty$），对偶不可行（$D^* = +\infty$），满足 $P^* = -D^*$。
5. 反例分析：详细展示了如果移除扩展理论中的任何一个约束条件（如允许同一行同时出现 $\infty$ 和 $-\infty$），强对偶定理或 Farkas 引理将失效。

5. 意义与影响 (Significance)

• 理论深度：该工作将线性规划对偶理论从标准的实数域扩展到了包含无限值的代数结构，为处理具有“硬”约束的离散优化问题提供了严格的数学基础。
• 形式化验证的标杆：这是首次在 Lean 4 中完整形式化包含无限系数的线性规划对偶理论。它展示了 Lean 4 处理复杂代数结构（如除环、模）和自定义算术规则（如扩展实数运算）的能力。
• 实际应用潜力：通过引入无限系数，优化问题中的“硬约束”（必须满足）和“软约束”（优化目标）可以统一在一个数学框架下处理，无需像传统方法那样进行繁琐的工程化转换（如设置一个极大的常数）。
• 对形式化社区的贡献：
  • 填补了 Mathlib 中关于“线性有序除环”和扩展实数运算的空白。
  • 提供了处理非标准矩阵乘法和无限值逻辑的通用模式，供后续研究者参考。
  • 证明了形式化方法不仅能验证已知定理，还能帮助发现新定理（如扩展 Farkas 引理的具体约束条件）并验证其边界情况。

总结：
这篇论文不仅成功地将经典的线性规划对偶理论形式化，更重要的是，它通过引入扩展实数域，解决了实际优化问题中“硬约束”建模的数学难题。作者通过严谨的 Lean 4 代码，证明了在引入无限值后，只要施加合理的约束条件，对偶理论依然保持其强大的数学结构。这项工作为形式化数学在运筹学和优化领域的应用开辟了新的方向。