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

Here is an explanation of the paper "Duality theory in linear optimization and its extensions: formally verified," translated into simple, everyday language with creative analogies.

The Big Picture: The "Mathematical Detective" and the "Infinite Ledger"

Imagine you are a detective trying to solve a mystery. The mystery is a Linear Program. In the real world, this is like trying to figure out the cheapest way to buy groceries while meeting specific nutritional needs (e.g., "I need at least 50g of protein, but I can't spend more than $10").

This paper is about two main things:

Proving the Rules: The authors used a computer program called Lean 4 to act as a super-strict judge. They wrote down the fundamental rules of how these "mysteries" work and forced the computer to check every single logical step to ensure the rules are 100% unbreakable.
Breaking the Rules (Gently): They took these rules and extended them to a weird new world where numbers can be Infinity ( $\infty$ ). This allows them to model "hard" constraints (like "I absolutely cannot eat peanuts") in a way that traditional math couldn't handle easily.

Part 1: The "Either/Or" Detective Work (Farkas' Lemma)

The core of the paper is based on a famous idea called Farkas' Lemma. Think of this as the ultimate "Either/Or" test for a system of equations.

The Analogy: The Alibi
Imagine a suspect (the solution) is accused of being in two places at once.

Scenario A: The suspect has a perfect alibi. There is a valid set of numbers (a solution) that satisfies all the rules.
Scenario B: The suspect is guilty. There is no solution. But how do you prove it? You find a "contradiction." You take the rules, mix them together like a cocktail, and end up with a statement that is obviously false, like "0 is less than 0."

The Theorem says: It is impossible for both to be true.

Either you can find a solution (the alibi holds).
OR you can find a mix of rules that creates a contradiction (the alibi is fake).
You can never have a situation where a solution exists and a contradiction exists simultaneously.

The authors proved this for standard math, and then they proved a "super version" of it that works even when the rules involve infinite values.

Part 2: The "Infinite Ledger" (Extended Reals)

Traditional math hates infinity. You can't really multiply or add it without breaking things. But in the real world, sometimes a constraint is so strict it feels infinite.

The Analogy: The "Hard" Constraint
Imagine you are planning a lunch.

Soft Constraint: "I want to spend as little as possible." (This is the goal).
Hard Constraint: "I am allergic to lentils."

In normal math, if you want to ban lentils, you might try to set the price of lentils to a huge number, like $1,000,000. But that's messy. What if you need $1,000,001? What if the allergy is really bad?

The authors introduced a new system called Extended Linearly Ordered Fields.

They added two special characters to the number line: $\top$ (Positive Infinity) and $\bot$ (Negative Infinity).
They defined rules for how these characters behave. For example, if you add "Positive Infinity" to "Negative Infinity," the Negative one wins (it's "stronger").
The Magic: Now, to say "No lentils allowed," you just set the price of lentils to $\top$ . The math naturally forces the solution to buy zero lentils, because buying any amount would make the total cost infinite.

This makes modeling "hard" constraints (like allergies or strict safety limits) much cleaner and more elegant.

Part 3: The "Shadow Price" (Duality)

The paper also deals with Strong Duality. This is a beautiful concept in optimization.

The Analogy: The Mirror World
Every optimization problem has a "twin" or a "mirror image" called the Dual Problem.

Primal Problem: "How do I buy the cheapest lunch?"
Dual Problem: "What is the value of every gram of protein and every calorie?"

The Strong Duality Theorem says: The answer to the Primal problem (the cost) is exactly the same as the answer to the Dual problem (the value of the ingredients), just flipped upside down.

Why does this matter?
If you solve the "lunch cost" problem, you automatically know the "value of nutrients." If the cost of a gram of protein goes up, you know exactly how much your lunch bill will increase. It's like looking in a mirror; the reflection tells you everything you need to know about the object.

The authors proved that this "Mirror World" relationship still holds true even when you use their new Infinity numbers.

Part 4: The "Robot Judge" (Formal Verification)

Why did they write this paper? Why not just write the math on a whiteboard?

The Analogy: The Code Review
Mathematicians have been doing this for centuries. But humans make mistakes. We get tired, we skip steps, or we assume something is "obvious" when it's actually tricky.

The authors used Lean 4, a programming language that is also a mathematical proof assistant.

They wrote the theorems in code.
The computer acted as a Robot Judge. It didn't care about "obvious" things. It demanded a proof for every single step.
If the logic had a tiny hole, the computer would scream "ERROR!" and refuse to accept the proof.

This paper is the result of that process. They didn't just say "Here is the proof." They said, "Here is the proof, and a computer has checked every single line of logic to ensure it is 100% correct."

Summary: What did they actually do?

They built a new math toolbox: They created a way to do linear algebra with Infinity included, specifically for "hard" constraints.
They proved the rules work: They showed that even with Infinity, the "Either/Or" detective rules (Farkas) and the "Mirror World" rules (Duality) still hold true.
They got a computer to sign off: They used Lean 4 to verify every step, ensuring there are no human errors in their logic.

The "Cheap Lunch" Example from the paper:
The authors used a real-world example: making a cheap lunch with rice and lentils.

Normal Math: If lentils go out of stock, you have to rewrite the whole math problem.
Their New Math: You just change the price of lentils to Infinity. The computer instantly recalculates the optimal lunch (which now contains only rice) without you having to rewrite the rules.

In short, they made the math of optimization more robust, more flexible, and mathematically bulletproof.

Here is a detailed technical summary of the paper "Duality theory in linear optimization and its extensions: formally verified" by Martin Dvorak and Vladimir Kolmogorov.

1. Problem Statement

The paper addresses the formal verification of duality theory in linear optimization, specifically focusing on two main challenges:

Generalization of Algebraic Structures: Standard duality theorems (like Farkas' Lemma and Strong Duality) are typically proven over linearly ordered fields (e.g., real numbers). The authors aim to generalize these results to linearly ordered division rings (where multiplication need not be commutative) and to handle systems with infinitely many equations.
Handling Infinite Coefficients: In discrete optimization and "hard" constraint problems, it is often necessary to model constraints that must be strictly satisfied or objectives that are infinitely penalized. Traditional Linear Programming (LP) cannot handle infinite values ( $\infty$ or $-\infty$ ) within the coefficient matrix or vectors. The authors seek to extend duality theory to extended linearly ordered fields ( $F_\infty = F \cup \{-\infty, +\infty\}$ ) to allow for a more direct mathematical formulation of problems with "hard" constraints without resorting to large finite approximations.

2. Methodology

The authors utilized the Lean 4 proof assistant and the Mathlib library to formally verify their theorems. Their methodology involved:

Formalizing Algebraic Hierarchies: They extended Mathlib's algebraic hierarchy to include Linearly Ordered Division Rings, which are not natively part of the standard library. This allowed them to prove theorems over non-commutative structures.
Defining Extended Structures: They defined an extended linearly ordered field $F_\infty$ by adding two elements, $\bot$ (negative infinity) and $\top$ (positive infinity). They carefully defined arithmetic operations (addition, negation, scalar multiplication) and order relations, noting that $F_\infty$ forms a densely linearly ordered abelian monoid but not a field (due to properties like $\bot + \top = \bot$ and $0 \cdot \bot = \bot$).
Custom Matrix/Vector Operations: Since standard Mathlib definitions for matrix-vector multiplication assume finite fields and standard commutativity, the authors implemented custom definitions (dotWeig, Matrix.mulWeig) to handle multiplication between vectors with values in $F_\infty$ and weights in $F$ .
Proof Strategy:
- Farkas-like Theorems: The proof of the most general Farkas theorem (fintypeFarkasBartl) relies on an inductive argument on the size of the finite type $J$ , following the approach of Bartl [Bar11].
- Extension to Infinity: The proof for the extended case (extendedFarkas) involves a reduction strategy: deleting rows/columns that contain tautologies or force variables to zero, and handling cases where $\bot$ appears in the constraint vector $b$ .
- Strong Duality: The strong duality theorem for extended LPs is derived by combining weak duality with the extended Farkas lemma, analyzing cases of feasibility, infeasibility, and unboundedness.

3. Key Contributions

A. Generalized Farkas Theorems

The authors proved a hierarchy of Farkas-like theorems, culminating in Theorem 1.6 (fintypeFarkasBartl). This theorem generalizes previous results by:

Allowing the underlying structure to be a linearly ordered division ring (non-commutative multiplication).
Supporting infinitely many equations (via linear maps from an arbitrary type $W$ ).
Allowing the target space of the linear map to be a linearly ordered module $V$ , rather than just the field itself.
Corollaries: This general result implies standard Farkas lemmas for matrices over fields, as well as Bartl's previous generalizations.

B. Extended Linear Programming (ELP)

The paper introduces a rigorous framework for LPs over $F_\infty$ :

Definition of Validity: They define a "Valid ELP" with six specific preconditions to ensure the duality theorem holds. These conditions prevent pathological interactions between $\bot$ and $\top$ (e.g., a row cannot contain both $\bot$ and $\top$ ; if $b_i = \top$ , $A_{ij}$ cannot be $\top$ ).
Strong Duality for ELP: They prove Theorem 1.11 (ValidELP.strongDuality), stating that for a valid ELP $P$ and its dual $D$ , if at least one is feasible, then $P^\star = -D^\star$ .
Necessity of Conditions: The authors provide counterexamples demonstrating that omitting any of the six validity conditions causes the strong duality theorem to fail.

C. Formal Verification

The entire development is formalized in Lean 4 (version 4.18.0) using Mathlib.
The code is publicly available, ensuring that every logical step is verified against the axioms of Lean (specifically propext, Classical.choice, and Quot.sound).

4. Results

Formal Proof of Generalized Duality: The authors successfully formalized the proof of fintypeFarkasBartl, which subsumes standard Farkas lemmas and Bartl's generalizations.
Extension to Infinite Coefficients: They proved extendedFarkas and ValidELP.strongDuality. These theorems allow for the direct modeling of "hard" constraints (e.g., setting a cost to $\infty$ to forbid a variable) within the duality framework.
Counterexamples: The paper rigorously establishes that the specific preconditions for the extended theorems are not merely technicalities but are mathematically necessary. Removing any single condition leads to scenarios where both the primal and dual systems have solutions (violating the "exactly one" property of Farkas lemmas) or where strong duality fails.
Practical Example: The "cheap lunch" example demonstrates how the extended theory handles a scenario where an ingredient (lentils) becomes unavailable. Instead of removing the variable, the cost is set to $\infty$ . The formal system correctly computes the new optimal solution and shadow prices without manual reformulation of the matrix dimensions.

5. Significance

Mathematical Rigor: The work provides the first machine-checked proofs of duality theory over linearly ordered division rings and extended fields, eliminating the possibility of human error in these complex algebraic manipulations.
Theoretical Unification: By proving theorems over division rings and modules, the authors unify various duality results that were previously treated as separate cases.
Practical Application in Optimization: The extension to infinite coefficients offers a mathematically elegant way to handle "hard" constraints in optimization problems. This is particularly relevant for Mixed-Integer Linear Programming (MILP) relaxations and constraint satisfaction problems where "soft" and "hard" constraints coexist.
Tooling for Lean/Mathlib: The project highlights both the strengths and current limitations of Lean 4. While the library excels at algebraic structures, the authors noted that matrix manipulation and case analysis over subtypes required significant ad-hoc machinery, suggesting areas for future library development.

In summary, this paper bridges the gap between abstract algebraic optimization theory and computer-verified mathematics, providing a robust foundation for reasoning about linear programs with infinite parameters and non-commutative coefficients.