4 ms·
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 pro
by gugagore 1y ago
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.
- 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...