[digama0]

Metamath has tactics, but they aren't part of metamath per se; they are part of the tools that you use to write proofs. You don't make the rest of the world run the same proof search you did hundreds of times, finding the same proof every time, when you could just write down the proof.

I'm aware this is an entirely unfair comparison. Coq and Metamath aren't doing anywhere near the same amount of stuff, so of course Metamath will be faster. But the question is: are you doing what is necessary? Is running omega all the time a requirement for large scale proof checking, or is it just the way Coq does things? I think you will find that it's not necessary in the abstract, but it's also pretty hard to write Coq any other way. (To be absolutely clear, I don't mean don't use omega, I mean use omega once and generate a proof, and don't make the rest of the world have to re-run your proof script.)

The sizes of things are actually hard to gauge in Metamath if you want to compare LOC to amount of human work, because what you see in a Metamath file are actually the output of some honest to goodness "tactic" or high level user interface. No one is writing asm here.

If you are not writing lemmas, and are relying on Coq tactics to rediscover the proof all the time, well, that's just demonstrably slow and redundant. In Metamath we use a combination of tactics to find proofs and optimizers to extract common lemmas and use the library of existing lemmas effectively; the Coq model leaves no space for the optimizer, so you get something... suboptimal.