Re: [Metamath] Codex wrote an MM verifier in Go pretty easily [AI Progress Report]

Wed, 17 Sep 2025 07:50:41 -0700 


> 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/C7CE9883-13F6-4F18-BF49-CB944A6D0A2B%40dwheeler.com.






















					Reply via email to