3 ms·
would you assess Metamath systems more robust in adversarial settings, because the verifier is so short?
by DoctorOetker 1mo ago
would you assess Metamath systems more robust in adversarial settings, because the verifier is so short?
- dwheeler 1mo agoMetamath is short, which does make it easier to verify. In addition, because it's simple, there are many implementions. The set.mm Metamath database, the most popular, is checked by 5 independently implemented proof verifiers.