I was curious if Codex could write a Metamath verifier, so asked ChatGPT for a list of verifiers and what languages it thought would be both *easy and interesting*: it chose Go.
I started from my mmverify.py repo (where iIhave a too-slow verifier in another weird language, MeTTa <https://metta-lang.dev/>), so it had access to reference implementations. The task was completed pretty easily (perhaps in 40-60min of AI-work) with my feeding in some errors. It seems to pass David Wheeler's Metamath-test suite <https://github.com/zariuq/metamath-test>. It's here if anyone's curious: https://github.com/zariuq/mmverify.py/tree/mmverifyGo/go FWIW, I decided to try to see if it could do Metamath Zero, and I must say it struggles (even to just do .mm0 + .mmu verification). -- 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/e55ea1ba-b3c2-4018-80a1-a46149ead54fn%40googlegroups.com.
