mmverify.py

As it happens, the Python verifier mmverify.py has an even simpler soundness bug [0], and so far I've reviewed two independent AI-written verifiers that have replicated that bug, since they apparently really like to copy the strategy from mmverify.py. A sound verifier isn't too difficult to write in terms of architecture (I just wrote one myself for differential testing [1]), but it requires some close attention to the details. That is to say, the Swiss-cheese approach definitely lends authority, but individual implementations are unfortunately not as foolproof as they're made out to be. [0] https://github.com/david-a-wheeler/mmverify.py/issues/30 [1] https://github.com/LegionMammal978/mm-verifier-tests/blob/ma...

Metamath's Python verifier - its trusted kernel - is just 700 lines of Python short: https://github.com/david-a-wheeler/mmverify.py/blob/master/m... Metamath Zero's Haskell implementation 700, and the C implementation 1000 lines (or 1800 overall) https://github.com/digama0/mm0 How do other proof systems compare? Some bug counts: https://tristan.st/blog/in_search_of_falsehood