---
OA_place: publisher
OA_type: hybrid
PlanS_conform: '1'
_id: '22607'
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\".\r\nCode:
    https://github.com/madvorak/duality/tree/v3.2.0"
acknowledgement: "We would like to thank David Bartl and Jasmin Blanchette for frequent
  consultations.\r\nWe would also like to express gratitude to Henrik Böving for a
  help with generalization\r\nfrom extended rationals to extended linearly ordered
  fields and to Andrew Yang for the\r\nproof of Finset.univ_sum_of_zero_when_not.
  We would also like to acknowledge Antoine\r\nChambert-Loir, Apurva Nakade, Yaël
  Dillies, Richard Copley, Edward van de Meent, Markus\r\nHimmel, Mario Carneiro,
  and Kevin Buzzard."
article_number: '14253'
article_processing_charge: Yes (in subscription journal)
article_type: original
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>Annals of Formalized Mathematics</i>. 2026;2. doi:<a
    href="https://doi.org/10.46298/afm.14253">10.46298/afm.14253</a>
  apa: Dvorak, M., &#38; Kolmogorov, V. (2026). Duality theory in linear optimization
    and its extensions -- formally verified. <i>Annals of Formalized Mathematics</i>.
    EPI Sciences. <a href="https://doi.org/10.46298/afm.14253">https://doi.org/10.46298/afm.14253</a>
  chicago: Dvorak, Martin, and Vladimir Kolmogorov. “Duality Theory in Linear Optimization
    and Its Extensions -- Formally Verified.” <i>Annals of Formalized Mathematics</i>.
    EPI Sciences, 2026. <a href="https://doi.org/10.46298/afm.14253">https://doi.org/10.46298/afm.14253</a>.
  ieee: M. Dvorak and V. Kolmogorov, “Duality theory in linear optimization and its
    extensions -- formally verified,” <i>Annals of Formalized Mathematics</i>, vol.
    2. EPI Sciences, 2026.
  ista: Dvorak M, Kolmogorov V. 2026. Duality theory in linear optimization and its
    extensions -- formally verified. Annals of Formalized Mathematics. 2, 14253.
  mla: Dvorak, Martin, and Vladimir Kolmogorov. “Duality Theory in Linear Optimization
    and Its Extensions -- Formally Verified.” <i>Annals of Formalized Mathematics</i>,
    vol. 2, 14253, EPI Sciences, 2026, doi:<a href="https://doi.org/10.46298/afm.14253">10.46298/afm.14253</a>.
  short: M. Dvorak, V. Kolmogorov, Annals of Formalized Mathematics 2 (2026).
corr_author: '1'
das_tickbox: '0'
date_created: 2026-07-29T09:06:55Z
date_published: 2026-03-13T00:00:00Z
date_updated: 2026-07-29T10:50:17Z
day: '13'
ddc:
- '500'
department:
- _id: VlKo
- _id: GradSch
doi: 10.46298/afm.14253
external_id:
  arxiv:
  - '2409.08119'
has_accepted_license: '1'
intvolume: '         2'
keyword:
- Farkas lemma
- linear programming
- extended reals
- calculus of inductive constructions
language:
- iso: eng
mathsc:
- 68V20
- 15A39
- 90C05
month: '03'
oa_version: Published Version
publication: Annals of Formalized Mathematics
publication_identifier:
  eissn:
  - 3117-4604
publication_status: published
publisher: EPI Sciences
quality_controlled: '1'
related_material:
  record:
  - id: '20071'
    relation: earlier_version
    status: public
researchdata_availability: no
status: public
supplementarymaterial: no
title: Duality theory in linear optimization and its extensions -- formally verified
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
  name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
  short: CC BY (4.0)
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 2
year: '2026'
...