---
OA_place: repository
OA_type: green
_id: '20071'
abstract:
- lang: eng
  text: 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".
acknowledgement: We would like to thank David Bartl and Jasmin Blanchette for frequent
  consultations. We would also like to express gratitude to Andrew Yang for the proof
  of Finset.univ sum of zero when not and to Henrik B¨oving for a help with generalization
  from extended rationals to extended linearly ordered fields. We would also like
  to acknowledge Antoine Chambert-Loir, Apurva Nakade, Ya¨el Dillies, Richard Copley,
  Edward van de Meent, Markus Himmel, Mario Carneiro, and Kevin Buzzard.
article_number: '2409.08119'
article_processing_charge: No
arxiv: 1
author:
- first_name: Martin
  full_name: Dvorak, Martin
  id: 40ED02A8-C8B4-11E9-A9C0-453BE6697425
  last_name: Dvorak
  orcid: 0000-0001-5293-214X
- first_name: Vladimir
  full_name: Kolmogorov, Vladimir
  id: 3D50B0BA-F248-11E8-B48F-1D18A9856A87
  last_name: Kolmogorov
citation:
  ama: Dvorak M, Kolmogorov V. Duality theory in linear optimization and its extensions
    -- formally  verified. <i>arXiv</i>. doi:<a href="https://doi.org/10.48550/arXiv.2409.08119">10.48550/arXiv.2409.08119</a>
  apa: Dvorak, M., &#38; Kolmogorov, V. (n.d.). Duality theory in linear optimization
    and its extensions -- formally  verified. <i>arXiv</i>. <a href="https://doi.org/10.48550/arXiv.2409.08119">https://doi.org/10.48550/arXiv.2409.08119</a>
  chicago: Dvorak, Martin, and Vladimir Kolmogorov. “Duality Theory in Linear Optimization
    and Its Extensions -- Formally  Verified.” <i>ArXiv</i>, n.d. <a href="https://doi.org/10.48550/arXiv.2409.08119">https://doi.org/10.48550/arXiv.2409.08119</a>.
  ieee: M. Dvorak and V. Kolmogorov, “Duality theory in linear optimization and its
    extensions -- formally  verified,” <i>arXiv</i>. .
  ista: Dvorak M, Kolmogorov V. Duality theory in linear optimization and its extensions
    -- formally  verified. arXiv, 2409.08119.
  mla: Dvorak, Martin, and Vladimir Kolmogorov. “Duality Theory in Linear Optimization
    and Its Extensions -- Formally  Verified.” <i>ArXiv</i>, 2409.08119, doi:<a href="https://doi.org/10.48550/arXiv.2409.08119">10.48550/arXiv.2409.08119</a>.
  short: M. Dvorak, V. Kolmogorov, ArXiv (n.d.).
corr_author: '1'
date_created: 2025-07-23T11:21:52Z
date_published: 2024-09-12T00:00:00Z
date_updated: 2026-03-27T12:36:59Z
day: '12'
department:
- _id: GradSch
- _id: VlKo
doi: 10.48550/arXiv.2409.08119
external_id:
  arxiv:
  - '2409.08119'
keyword:
- Farkas lemma
- linear programming
- extended reals
- calculus of inductive constructions
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://doi.org/10.48550/arXiv.2409.08119
month: '09'
oa: 1
oa_version: Preprint
publication: arXiv
publication_status: draft
related_material:
  link:
  - description: full version of all definitions, statement, and proofs
    relation: software
    url: https://github.com/madvorak/duality/tree/v3.2
  record:
  - id: '21393'
    relation: dissertation_contains
    status: public
status: public
title: Duality theory in linear optimization and its extensions -- formally  verified
type: preprint
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
year: '2024'
...