@article{22607,
  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".
Code: https://github.com/madvorak/duality/tree/v3.2.0},
  author       = {Dvorak, Martin and Kolmogorov, Vladimir},
  issn         = {3117-4604},
  journal      = {Annals of Formalized Mathematics},
  keywords     = {Farkas lemma, linear programming, extended reals, calculus of inductive constructions},
  publisher    = {EPI Sciences},
  title        = {{Duality theory in linear optimization and its extensions -- formally verified}},
  doi          = {10.46298/afm.14253},
  volume       = {2},
  year         = {2026},
}