Metamath's state is a little amazing; it's tied for third place, yet there is very little built in. For example, numbers are not built-in, they are a derived construct. Metamath didn't even have a decimal number representation until 2015. When you truly start with just logic and set theory (specifically ZFC) it's a lot of work to get to just the basics, especially when you have to directly show every step. Each of the systems listed here are worthy systems. I work most with Metamath; this video I created explains more about its background: https://www.youtube.com/watch?v=8WH4Rd4UKGE
I think mathematical formalization is important, and in the long term that needs to be the direction of mathematics in general. It's too easy to make "proofs" that have errors that slip by. Automated theorem verification systems don't get tired and give far more confidence that proofs really are proofs. If math is all about proving that certain claims can be proven from well-accepted assumptions, then we need to make those proofs more rigorous.
I really like how Metamath sits on an extreme edge; its underlying formalization is simple, to the point where a relatively short Python script [0] is sufficient to do verification, and this also massively increases confidence, at the meta-level, in the correctness of the entire endeavor.
I wonder about how Metamath compares to wholly-constructive approaches common in abstract algebra, category theory, and computer science. I suspect that, much like Archimedes with his levers, a category theorist with a sufficiently-large blackboard could draw a diagram to constructively prove anything that they like, and it's unfortunate that this style of argument is not compatible with current formal methods.
Very much agreed, and V. Voevodski has expressed authentic concern from the working mathematician side that peer review needs machine help. Wiedijk writings are nice. I have taken a look at Mizar articles and they are a fantastic sample of good things already achieved. We need to close the usability gap so writing formalizations is just easier. We need a big open source project, the Linux of mathematical vernacular.
I wonder about the status of Raph Levien's Ghilbert [1]. It seemed an approachable proxy to Metamath, promising enough that I thought I can persuade my mathematician friends to look at it sooner or later.
That's certainly true for Metamath; once the progress of Metamath was tracked against this list of 100 theorems (around 2014), a lot more theorems from the 100 theorems list were added of course: https://docs.google.com/spreadsheets/d/1jcLOp_jF4sPrVPdPedL_... but in fact more proven theorems were added in general: https://docs.google.com/spreadsheets/d/1TnuBekyUP918smZeJRD0...
Metamath's state is a little amazing; it's tied for third place, yet there is very little built in. For example, numbers are not built-in, they are a derived construct. Metamath didn't even have a decimal number representation until 2015. When you truly start with just logic and set theory (specifically ZFC) it's a lot of work to get to just the basics, especially when you have to directly show every step. Each of the systems listed here are worthy systems. I work most with Metamath; this video I created explains more about its background: https://www.youtube.com/watch?v=8WH4Rd4UKGE
I think mathematical formalization is important, and in the long term that needs to be the direction of mathematics in general. It's too easy to make "proofs" that have errors that slip by. Automated theorem verification systems don't get tired and give far more confidence that proofs really are proofs. If math is all about proving that certain claims can be proven from well-accepted assumptions, then we need to make those proofs more rigorous.