5 ms·

That's with the original C verifier only. The actual database is cross-checked by 6 independent implementations. This is the whole point of Metamath: its kernel

That's with the original C verifier only. The actual database is cross-checked by 6 independent implementations. This is the whole point of Metamath: its kernel is so tiny that you can implement a verifier in a weekend. Metamath isn't a silver bullet in the design space of formal proof tools, but I personally think it just about nails the metatheory we want. Maybe some explicit facility around definitions would be desireable.

i2talics 2mo ago
Why does the original C verifier have bugs if its supposedly so easy to implement a verifier?
- poizan42 2mo ago
  Nothing more complex than Hello world is easy to implement in C without risking mistakes in checking boundary conditions if you are not really careful.
- xelxebar 2mo ago
  Ease of implementation means we get more, independent verifiers rather than trusting any particular one.
LegionMammal978 2mo ago
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 https://github.com/david-a-wheeler/mmverify.py/issues/30 [1] https://github.com/LegionMammal978/mm-verifier-tests/blob/main/mmreference.py https://github.com/LegionMammal978/mm-verifier-tests/blob/ma...