Syntax-only formalisms are faster than semantically-laden formalisms; a compiler's parser is usually faster than its backend. Metamath is going to always be fas

Syntax-only formalisms are faster than semantically-laden formalisms; a compiler's parser is usually faster than its backend. Metamath is going to always be faster than Coq, Lean, Isabelle, HOL, Agda, Idris, or indeed much weaker systems like Haskell. There's no RSI in working with Metamath. What I mean is that the workflow is largely dependent on me knowing what I want to prove and roughly how I want to prove it, rather than Metamath chewing CPU.