We should look at this in the context. I see Metamath as an assembler language, so it's more detailed. If you look at high level tactics language of type theory PAs like Lean and Coq then their proofs may be shorter at the expense of the detail. But if those tactics were expanded then their proofs will become a whole mess which is difficult to understand. So, to be competitive Metamath's proofs should be detailed and clear at the same time. Unfortunately there is no help from available tools to achieve that goals and it's just an art or black magic at the moment.
-- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/812c0a0c-d0a5-4a36-ad06-d1fef5f4e946%40googlegroups.com.
