This is very cool work, and I'm happy to see it. I've been fascinated with Metamath for a very long time, finding its simplicity extremely appealing, and have a

This is very cool work, and I'm happy to see it. I've been fascinated with Metamath for a very long time, finding its simplicity extremely appealing, and have also made a number of attempts (under the Ghilbert name) to fix the problems Mario so eloquently identifies. But I never quite got it to gel. It's clear Mario has the technical chops, and I hope this publication gets the MM family a little more academic respectability and notice.