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

TL;DR

This paper formally verifies Farkas-like theorems and extends duality theory in linear optimization to include infinite coefficients using Lean 4, ensuring rigorous mathematical correctness.

Contribution

It provides the first formal proof of Farkas-like theorems over ordered fields and extends duality theory to infinite coefficients in a proof assistant.

Findings

Formal proof of Farkas-like theorems over ordered fields

Extension of duality theory to infinite coefficients

Implementation in Lean 4 for rigorous verification

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".