Skip to content
Source of metamath book
TeX Other
  1. TeX 99.7%
  2. Other 0.3%
Branch: master
Clone or download
nmegill Merge pull request #221 from metamath/errata2
Errata: Note that "To undo..." after assign no longer displays
Latest commit 44598e6 Aug 9, 2019
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
cover
.travis.yml
LICENSE.md Switch to Creative Commons CC0 license Jan 30, 2019
README.md Improve errata, fix #218 Jun 30, 2019
abstract.txt
allowed-errors
errata.md
generate-pdf
kindle-changes.patch
make-narrow
metamath.tex
narrow.sty
normal.sty
special-settings.sty Add the ability to generate metamath-narrow.pdf for smartphones etc. Jan 24, 2019

README.md

metamath-book

Build Status

This is the LaTeX editable source of the book Metamath: A Computer Language for Pure Mathematics, also known as the Metamath book. This book provides an in-depth understanding of the Metamath language and program. The first part of the book also includes an easy-to-read informal discussion of abstract mathematics and computers, with references to other proof verifiers and automated theorem provers.

This material is released to the public domain (no copyright) worldwide per the Creative Commons CC0 1.0 Universal (CC0 1.0) Public Domain Dedication; here is our copy of the CC0 license. This license has the SPDX license identifier CC0-1.0. However, although it is not a legal requirement, we do ask that you give credit.

Note: In December 2018, the predicate calculus axioms were renumbered and no longer match those in Sections 3.3.2 and 3.3.3 of the 2014 version of the book. A cross reference between the new and old numbers can be found in Appendix 8 of the Metamath Proof Explorer Home Page.

Get your printed copy!

You can get your very own printed copy of the 2019 hardback via Lulu

Errata

Errata for the 2019 Metamath book is available. If you prefer, you can see the errata in raw text form.

Editing

To edit the text, simply edit file metamath.tex.

If you generate example displays from the Metamath program, use 61 characters per line (you can use the command set width 61 to do this).

Generating a PDF

The source is in LaTeX format. To generate a PDF, you first need to install

  • The programs pdflatex, bibtex, makeindex
  • The style file anysize.sty

On Ubuntu, you can install all prerequisites by installing these packages:

  • texlive-fonts-recommended
  • texlive-latex-extra
  • texlive-fonts-extra
  • dvipng
  • texlive-latex-recommended

On Cygwin, you can install all prerequisites by installing these packages:

  • texlive
  • texlive-collection-latex
  • texlive-collection-latexextra
  • texlive-collection-bibtexextra
  • texlive-collection-latexrecommended

On a Unix-like system you can simply run the script ./generate-pdf to generate a normal PDF (or ./make-narrow to generate a narrow version). To generate both, run the commands sequentially in this order (you have to run make-narrow first):

./make-narrow
./generate-pdf

See the file metamath.tex for detailed instructions how to generate a PDF file by hand.

Citation

BibTeX citation:

@Book{metamath,
author = {Norman D. Megill and David A. Wheeler},
title = {Metamath: A Computer Language for Pure Mathematics},
year = {2019},
publisher = {Lulu Press},
address = {Morrisville, North Carolina},
url = {http://us.metamath.org/downloads/metamath.pdf},
note = {{\tt http://us.metamath.org/downloads/metamath.pdf}},
}

Narrow width screens

You can run ./generate-pdf narrow to generate "metamath-narrow.pdf", a version of the PDF formatted for narrow-width screens such as mobile phones.

The narrow version is based on an old version of this book that was generated specifically for narrow-width screens called the "Kindle version" by John D. Baker in 2011. The changes that implemented the Kindle version are in file kindle-changes.patch. We keep the .patch file around so that we might be able to borrow more of its ideas in the future.

Contributions

We love contributions! If you have an improvement for the text, or for generation (such as improving how metamath-narrow.pdf works), please create a pull request. Contributions must be under the same license (release to the public domain under CC0).

You can’t perform that action at this time.