2024/09/12 by Dvorak, Martin, Kolmogorov, Vladimir
#FOS: Computer and information sciences #FOS: Mathematics #Logic in Computer Science (cs.LO) #Optimization and Control (math.OC)
paper · doi:10.48550/arxiv.2409.08119
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''.