eBook (PDF), 211 Pages
(1 Ratings)
Price: Free
Metamath is a tiny computer language that can express theorems in abstract mathematics, accompanied by proofs that can be verified by a computer program. The first part of the book provides easy-to-read informal discussion of abstract mathematics and computers for general audiences. The later parts provide in-depth coverage of the foundations of mathematics, the Metamath language, and the Metamath program. More information can be found at the Metamath web site.
Available in PDF Format

Ratings & Reviews

Log in to review this item
2 People Reviewed This Product
  • By knambiar
    Dec 20, 2009
    The book under review titled "Metamath" by author Norman Megill contains five chapters, four appendices and has 196+15 pages. Chapter headings: 1. Introduction 2. Using the Metamath Program 3. Abstract Mathematics Revealed 4. The Metamath Language 5. The Metamath Program Appendix headings: A. Math Symbols Tokens for Set Theory B. Compressed Proofs C. Metamath's Formal System D. The MIU System The MIU in the last appendix refers to a tiny example of a formal system defined by Douglas Hofstadter, which explains all the critical terminology needed to understand an axiomatic theory. If any technical term in the rest of this review turns out incomprehensible, please use the Google search box. The name Metamath like Fortran refers to both a language and a program, the difference is that while Fortran program carries out numerical calculations, Matamath program verifies formal proofs of theorems. Lest one might think that Metamath is a program to verify proofs of theorems like... More > 1+1=2 as in Principia Mathematica, I hasten to add that this is far from true. When I once made a proposal (type "definition of intuitive set theory" without quotes in Google search box) that the cardinality of the class of all subsets of $aleph_{alpha}$ of cardinality $aleph_{alpha}$ should be taken as equal to $2^{aleph_alpha}$ Metamath was able to show with a Principia Mathematica type proof that this can be proved as a theorem and hence will not introduce any inconsistency in ZF theory. Ever since this happened, I have considered Metamath as one of the most significant achievements of the 21st century, just as I consider Principia Mathematica as the most significant advance of the 20th century. A remarkable fact is that Metamath achieves all this with a tiny program of less than 3MB size, which you can download from the Metamath site (type "" in Google search box). Installation of the program is dead easy, just unzip the downloaded file in a directory (any directory) of your choice and verify that important files like,, and are in there. The file is the set theory database and is for demonstration. Remember that Metamath has a standard command line interface and you have to use the Command Prompt if you are using Windows. If you ever want to uninstall Metamath, just delete the directory and no trace of the program will be left behind in the computer. So far we have been carried away by the program Metamath, but this review is about the book Metamath. The book has one of the clearest exposition of the set theory possible and it builds up set theory in a most appealing way. As an instructor of computer science, I had always wanted to give the definition of ZFC theory in the easiest way possible and this the book has accomplished with admirable simplicity. Here is the sequence of exposition given in two pages of the book (pp. 64-65): 1. Propositional Calculus (three axioms and modus ponens) 2. Predicate Calculus (four axioms and the rule of generalization) 3. Equality and Substitution (ten axioms) 4. ZFC Theory (seven axioms including the axiom of choice) All the axioms are explained in plain English making it clear that set theory becomes complex only when we deal with infinite sets. The Metamath book is the handbook for using the Metamath program, like the TeXbook of Donald Knuth being the handbook for using the TeX typesetting program. The similarity does not end there, while TeXbook is typeset with TeX, Metamath is typeset using LaTeX. Metamath uses LaTeX almost to perfection, except that the unavoidable "orphans and widows" do occur in some places. But then, it should be recognized that this is a flaw which practically no author can avoid. The author allows a free download of Methmath book, but as a serious user, I have a printed copy (2007 edition) for myself. Here is my suggestion for a quick start for you, assuming that you have already downloaded and installed Metamath under Windows. 1. If you have arranged everything nicely, a double click on metamath.exe in the metamath folder will take you to the MM> prompt in the command line interface. The black window will have the Metamath prompt MM> ready to execute your command. Go to page 40 of Metamath book and start with the section 2.3 A Trial Run. Gain some familiarity with all the MM> commands in this section by actually executing them. 2. Once you are at ease with the MM> commands, go to page 46 and start with the section 2.4 Your First Proof. If you execute all the MM-PA> commands in this section you will have a good idea what a Proof Assistant (PA) is. It is the business of the PA to dissect your theorem and make sure that the theorem has not violated the axioms of your theory. That's it. The rest are all merely a matter of scale and details. Before I conclude this review, one more complimentary statement about Metamath book. The author makes the LaTeX template he has used, actually the whole .tex file, available for you to download free. In fact, everything the author has done is in the Public Domain. Is this not what we are all supposed to do, and take the credit when it is thrust on you, and not demand it?< Less
  • By Josh Purinton
    May 28, 2007
    "Highly recommended" 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.
There are no reviews for previous versions of this product

Product Details

Norman Megill
October 1, 2011
File Format
File Size
1.34 MB
Product ID

Formats for this Ebook

Required Software Any PDF Reader, Apple Preview
Supported Devices Windows PC/PocketPC, Mac OS, Linux OS, Apple iPhone/iPod Touch... (See More)
# of Devices Unlimited
Flowing Text / Pages Pages
Printable? Yes
Report This Content to Lulu >

Moderation of Questionable Content

Thank you for your interest in helping us moderate questionable content on Lulu. If you need assistance with an order or the publishing process, please contact our support team directly.

How does this content violate the Lulu Membership Agreement?


Listed In

More From Norman Megill

Metamath Metamath By Norman Megill Paperback: