The only source I am aware of is https://github.com/david-a-wheeler/metamath-test and the metamath-exe test suite (https://github.com/metamath/metamath-exe/tree/master/tests). Collecting failing tests and serving as a unit test for new verifiers is part of the stated purpose of the former repository, so perhaps that answers your question.
On Fri, Mar 10, 2023 at 5:00 PM Samuel Goto <samuelg...@gmail.com> wrote: > 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 metamath+unsubscr...@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/63400cee-5e0e-4b16-9c80-fc4ed8b430ddn%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/63400cee-5e0e-4b16-9c80-fc4ed8b430ddn%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSvY-oggjiATKMa5Co7OukNb5nQSS3PUKp1wqytxFeLBsw%40mail.gmail.com.
