Coincidentally, by running it on one of my test files, I just noticed that mmverify.py suffers from the exact same issue <https://github.com/david-a-wheeler/mmverify.py/issues/30> of allowing proofs to reference inactive hypotheses belonging to other theorems. Centralizing all the test suites probably would be a good idea.
On Wed, Sep 17, 2025 at 10:32 AM David A. Wheeler <[email protected]> wrote: > > > > On Sep 16, 2025, at 6:42 PM, Jim Kingdon <[email protected]> wrote: > > > > Those all sound like good things to add to the testsuite. > > Patches welcome :-) to: > https://github.com/david-a-wheeler/metamath-test > > > > (The tests in the metamath-exe and metamath-knife repos are I think > better developed, although in principle some of their tests could be fed > back to a testsuite which could be run on any verifier). > > That was my goal for metamath-test. I also think it's useful to have a > "general" test suite. > > I'd be happy to contribute that repo to the https://github.com/metamath > organization. They're all MIT licensed, allowing anyone do practically > anything except sue the authors. Anyone want me to do that? > > > On September 16, 2025 12:44:47 PM PDT, Matthew House < > [email protected]> wrote: > > A few issues I spotted, many of which are nitpicks and some of which are > more serious:... > ... > > Writing a correct Metamath verifier requires very careful attention to > detail, which it seems that LLMs still struggle with, short of directed > hand-holding or extraordinarily thorough test suites. The original > mmverify.py code is quite compact for how many details it captures. > > > LLMs can be a *great* productivity aid, but only an *aid*. The emerging > term is "AI Code Assistant" which I think gives the right flavor. They are > helpful *assistants* to humans, but at least so far, they are not > *replacements* for humans. > > --- David A. Wheeler > > > -- 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 visit https://groups.google.com/d/msgid/metamath/CADBQv9bSGMebPM3QtCDFqfwfobCXj63c%3DyijPc65kXLq9g0vcQ%40mail.gmail.com.
