Duality theory in linear optimization and its extensions -- formally verified
Optimization and Control
2026-03-18 v3 Logic in Computer Science
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".
Cite
@article{arxiv.2409.08119,
title = {Duality theory in linear optimization and its extensions -- formally verified},
author = {Martin Dvorak and Vladimir Kolmogorov},
journal= {arXiv preprint arXiv:2409.08119},
year = {2026}
}
Comments
Code: https://github.com/madvorak/duality/tree/v3.2.0