Duality theory in linear optimization and its extensions -- formally verified
<|reference_start|>Duality theory in linear optimization and its extensions -- formally verified: 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''.<|reference_end|>
@article{dvorak2024duality,
    title={Duality theory in linear optimization and its extensions -- formally
  verified},
    author={Martin Dvorak and Vladimir Kolmogorov},
    journal={arXiv preprint arXiv:2409.08119},
    year={2024},
    archivePrefix={arXiv},
    eprint={2409.08119},
    primaryClass={math.OC cs.LO}
}