Duality theory in linear optimization and its extensions -- formally verified
Dvorak M, Kolmogorov V. 2026. Duality theory in linear optimization and its extensions -- formally verified. Annals of Formalized Mathematics. 2, 14253.
Download
No fulltext has been uploaded. References only!
Journal Article
| Published
| English
Corresponding author has ISTA affiliation
Department
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
Publishing Year
Date Published
2026-03-13
Journal Title
Annals of Formalized Mathematics
Publisher
EPI Sciences
Acknowledgement
We would like to thank David Bartl and Jasmin Blanchette for frequent consultations.
We would also like to express gratitude to Henrik Böving for a help with generalization
from extended rationals to extended linearly ordered fields and to Andrew Yang for the
proof of Finset.univ_sum_of_zero_when_not. We would also like to acknowledge Antoine
Chambert-Loir, Apurva Nakade, Yaël Dillies, Richard Copley, Edward van de Meent, Markus
Himmel, Mario Carneiro, and Kevin Buzzard.
Volume
2
Article Number
14253
eISSN
IST-REx-ID
Cite this
Dvorak M, Kolmogorov V. Duality theory in linear optimization and its extensions -- formally verified. Annals of Formalized Mathematics. 2026;2. doi:10.46298/afm.14253
Dvorak, M., & Kolmogorov, V. (2026). Duality theory in linear optimization and its extensions -- formally verified. Annals of Formalized Mathematics. EPI Sciences. https://doi.org/10.46298/afm.14253
Dvorak, Martin, and Vladimir Kolmogorov. “Duality Theory in Linear Optimization and Its Extensions -- Formally Verified.” Annals of Formalized Mathematics. EPI Sciences, 2026. https://doi.org/10.46298/afm.14253.
M. Dvorak and V. Kolmogorov, “Duality theory in linear optimization and its extensions -- formally verified,” Annals of Formalized Mathematics, vol. 2. EPI Sciences, 2026.
Dvorak M, Kolmogorov V. 2026. Duality theory in linear optimization and its extensions -- formally verified. Annals of Formalized Mathematics. 2, 14253.
Dvorak, Martin, and Vladimir Kolmogorov. “Duality Theory in Linear Optimization and Its Extensions -- Formally Verified.” Annals of Formalized Mathematics, vol. 2, 14253, EPI Sciences, 2026, doi:10.46298/afm.14253.
Material in ISTA:
Earlier Version
arXiv 
Google Scholar