4 ms·
A tool to verify estimates, II: a flexible proof assistant
- black_13 1y ago[dead]
- gugagore 1y agoI 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.
- nh23423fefe 1y agotao answered in comments https://terrytao.wordpress.com/2025/05/09/a-tool-to-verify-estimates-ii-a-flexible-proof-assistant/#comment-688007 https://terrytao.wordpress.com/2025/05/09/a-tool-to-verify-e...
- proof_by_vibes 1y agoRelated 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...