How would you improve it? (Also note that this is not the language mathematicians actually work with - that's more like https://www.youtube.com/watch?v=b-RfoUuQpAQ)

Similarly, for Metamath Zero, MM1 compiles down to the MM0 base language: https://www.youtube.com/watch?v=A7WfrW7-ifw

I think it's just a neat example that helps one understand how the verifier itself works at the most fundamental level.