Related to linear programming in theorem provers is this paper on Farkas' lemma implemented in Lean. It doubles as an interesting onboarding for working with some of the common abstractions found in Mathlib: https://github.com/madvorak/duality/blob/main/nonLean%2Fdual...