### Abstract

We formalize a proof of Motzkin's transposition theorem and
Farkas' lemma in Isabelle/HOL. Our proof is based on the
formalization of the simplex algorithm which, given a set of linear
constraints, either returns a satisfying assignment to the problem or
detects unsatisfiability. By reusing facts about the simplex algorithm
we show that a set of linear constraints is unsatisfiable if and only
if there is a linear combination of the constraints which evaluates to
a trivially unsatisfiable inequality.

BSD License