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

I wonder why not embed this in Lean or other theorem prover?

There is often a discussion drawn between a computer algebra system and an interactive theorem prover, but to be honest, I don't fully understand what the distinction means.

[dead]