Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Martin Dvorak, Vladimir Kolmogorov

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

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

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".
Paper Structure (25 sections, 13 equations)

This paper contains 25 sections, 13 equations.

Table of Contents

  1. Introduction
  2. Bartl's generalization
  3. Extension to infinite coefficients
  4. Example---cheap lunch
  5. Structure of this paper
  6. Preliminaries
  7. Review of algebraic typeclasses that our project depends on
  8. Extended linearly ordered fields
  9. Vectors and matrices
  10. Mathlib definitions versus our definitions
  11. Modules and how to order them
  12. Linear programming
  13. Formal statements of selected theorems
  14. Main corollaries
  15. Main results
  16. ...and 10 more sections