Duality theory in linear optimization and its extensions -- formally verified
This work provides formally verified foundations for linear optimization, which is incremental but crucial for ensuring correctness in mathematical proofs and computational applications.
The authors tackled the formal verification of Farkas' lemma and duality theory in linear optimization, extending it to include infinite coefficients, and successfully proved these theorems using Lean 4.
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".