3 ms·
That's not true for proofs in assistants like Coq, which work by generating a program whose type can be checked to verify the statement in question.
by njs12345 14y ago
That's not true for proofs in assistants like Coq, which work by generating a program whose type can be checked to verify the statement in question.