The problem with metamath is that you basically have to be a fully signed-up masochist in order to do anything nontrivial with it. People have certainly done nontrivial things with it e.g Carneiro and the prime number theorem -- but it takes all sorts. If I want to prove (a+b)(a+2b)(a+3b)= a^3 + 6ba^2 + 11b^2a + 6b^3 in Lean I just type `ring`. Good luck proving that from the axioms of a ring directly in metamath, I challenge you to do it in fewer than 30 moves. I should also say that whilst Metamath has certainly formalised a whole bunch of mathematics, it has not remotely gone "a long way" by any reasonable measure which a mathematician would use. For example, how much of an undergraduate mathematics curriculum does it have? How much representation theory? None. How much differential geometry? None. How much commutative algebra? Epsilon. These are the measures which mathematicians use, not lines of code. It is time that formalisation started to appeal to mathematicians, and for this to happen it is essential that it starts to demonstrate that it can actually do a lot of the kind of mathematics which is recognised as "completely standard undergraduate material and hence trivial" by mathematicians. It is still the case that these systems cannot do certain things which were known to Gauss or Euler (for example it was only this year that Lean learnt the proof that the class group of an imaginary quadratic field was finite, and as far as I know no other system at all has class groups -- but we teach this to the undergraduates!). Just saying "large code base therefore we've gone a long way" is not the correct logic. The question is how much of it is recognisable as worth teaching to undergraduates in 2021, and conversely how much stuff worth teaching to undergraduates in 2021 is _not_ in any of these systems. That's where the problems begin to show up. In Lean we are well into a project of formalising an entire undergraduate curriculum and within about two years we will have finished.
> The problem with metamath is that you basically have to be a fully signed-up masochist in order to do anything nontrivial with it. People have certainly done nontrivial things with it e.g Carneiro and the prime number theorem -- but it takes all sorts. If I want to prove (a+b)(a+2b)(a+3b)= a^3 + 6ba^2 + 11b^2a + 6b^3 in Lean I just type `ring`. Good luck proving that from the axioms of a ring directly in metamath, I challenge you to do it in fewer than 30 moves.
While it's allowed, generally Metamath users do not prove constructs directly from axioms, for exactly the same reason as you don't do it in Lean or traditional informal mathematics. You're right that most Metamath tools have fewer automated tactics, but there are tools with some automation, and people are working to improve that.
