Among all the languages for representing mathematical proofs, Metamath stands alone in its simplicity and elegance. This book begins by describing the need for a system like Metamath and the author's inspiring journey towards creating it. It continues with a step-by-step guide to using the metamath program to write and check proofs and ends with a precise description of the Metamath formal system itself. As a bonus, an appendix formalizes Hofstadter's MIU system in Metamath and shows how to derive "MUIIU".

This is an excellent, one-of-a-kind book. To anyone wishing to understand abstract mathematics from first principles in a completely rigorous way, I say: this is the book for which you've been waiting.