It seems that metamath's representation is a basic primitive for encoding maths at a syntactic level. It uses simple rules to recursively apply syntactical substitution transformations in order to build up a kind of complete, ostensibly true statement. A statement that is encoded in a way that a small proven-true statement checker can ~linearly (!) follow along the statement of the proof and find it logically sound. It seems weird to me that it's even possible to cross the boundary from syntactic representation to semantic meaning so seamlessly.
