Hey all,
I'm wondering: is there any chance anyone has built a list of proofs
that are expected to fail to check verifiers?
Context: as I'm trying to verify some of the disjoint variable
restrictions, I'm finding that I'm missing a lot of corner cases I missed
from the book/specification, and when I do, verifications succeeds rather
than fails, and I have to manually catch those bugs. So, if I'm thinking
that if had a list of proofs that have known bugs (for the $d statement
specifically, but more generally too) that a valid verifier would
successfully catch, I'd feel more comfortable knowing that I've captured
known ways a proof is invalid.
Anyone?
Sam
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/63400cee-5e0e-4b16-9c80-fc4ed8b430ddn%40googlegroups.com.
