A tool to verify estimates, II: a flexible proof assistant terrytao.wordpress.com 55 points by jjgreen 4 days ago
gugagore 2 minutes 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.
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]