If you're interested in the main book on Metamath, it is "Metamath: A Computer Language for Mathematical Proofs" by Norman Megill & David A. Wheeler. You can g

If you're interested in the main book on Metamath, it is "Metamath: A Computer Language for Mathematical Proofs" by Norman Megill & David A. Wheeler. You can get the hardcover here: http://www.lulu.com/shop/norman-megill-and-david-a-wheeler/metamath-a-computer-language-for-mathematical-proofs/hardcover/product-24129769.html http://www.lulu.com/shop/norman-megill-and-david-a-wheeler/m... Full disclosure: I'm one of the co-authors.