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 sufficien

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. [0] http://us.metamath.org/downloads/mmverify.py http://us.metamath.org/downloads/mmverify.py