3 ms·
“Formal proof” and “mechanized proof” are not synonymous. And proof assistants have a long way to go before they can be useful for mathematics in general.
by catnaroek 9y ago
“Formal proof” and “mechanized proof” are not synonymous. And proof assistants have a long way to go before they can be useful for mathematics in general.
- johnbender 9y agoYes! I’m not suggesting they are synonymous, but proofs in coq are definitely formal proofs (as I understand that term/phrase).