# Duality theory in linear optimization and its extensions -- formally verified

arXiv: https://arxiv.org/abs/2409.08119 · HTML: https://mlsanity.com/paper/2409.08119/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 12 Sep 2024.

## Built on by (most cited first, 1 of 1)

- [CLASSO: a practical primal path-following algorithm for the constrained LASSO](https://mlsanity.com/paper/2610.17024/) (2026)

## Abstract (arXiv)

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".