Papers With

← All papers
First page of Duality theory in linear optimization and its extensions – formally verified

Duality theory in linear optimization and its extensions – formally verified

Martin Dvorak, Vladimir Kolmogorov

math.OC Sep 12, 2024 · v3 cs.LO
formalization mathlib algebra
Read PDF arXiv abstract Code
TL;DR
Formalizes Farkas-like theorems, strong LP duality, and a new extension to extended linearly ordered fields in Lean 4 with Mathlib.
Abstract
Farkas established that a system of linear inequalities has a solution if and only if we cannot obtain a contradiction by taking a linear combination of the inequalities. We state and formally prove several Farkas-like theorems over linearly ordered fields in Lean 4. Furthermore, we extend duality theory to the case when some coefficients are allowed to take "infinite values".
Problem

Farkas-type theorems of alternatives and strong LP duality are foundational in linear optimization. The goal is to formally verify them over general linearly ordered fields and to extend duality theory to coefficients that may take infinite values.

Approach

Using Lean 4.18.0 and Mathlib, the authors first prove a Farkas–Bartl theorem over linearly ordered division rings and modules by induction. They derive equality and inequality Farkas lemmas and strong LP duality from it as corollaries. They define extended linearly ordered fields with ⊥ and ⊤ and prove an extended Farkas theorem and extended weak and strong LP duality under side conditions on where infinities may appear.

Results

All theorems are machine-checked, using only the axioms propext, Classical.choice and Quot.sound. Counterexamples show that each precondition of the extended Farkas theorem is necessary.