3 ms·
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 so
by proof_by_vibes 1y ago
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%2Fduality.pdf https://github.com/madvorak/duality/blob/main/nonLean%2Fdual...