Duality theory in linear optimization and its extensions -- formally verified
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
Fields of Study & Subjects
Formal Methods in Verification
Advanced Control Systems Optimization
Advanced Optimization Algorithms Research
Publication details
- Journal / source
- Annals of Formalized Mathematics
- Volume
- Volume 2
- Publication date
- 13 March 2026
- Language
- EN