Elamur Research⌕
☰
home / papers / 2019 / Metamath: A Computer Language for Mathematical Proofs

Metamath: A Computer Language for Mathematical Proofs

Paper · 2019 · Norman Megill and David A. Wheeler

Summary

This book introduces Metamath, a deliberately minimal computer language for writing fully formal mathematical proofs that a machine can check. The authors aim to make every proof step explicit so that a proof can be trusted without relying on a mathematician's intuition or on a complex prover. In Metamath, a small set of statement types declares symbols, axioms and theorems, and checking a proof reduces to applying substitutions step by step. The book compares Metamath with computer algebra systems, automated and interactive theorem provers, and other proof verifiers. It then shows how logic and ZFC set theory, and from them real and complex numbers, can be built from a short list of axioms, as done in the set.mm database. Later chapters give a full specification of the language and a reference manual for the Metamath program. The work matters because a very simple verifier, combined with a large public database of formalized mathematics, provides a highly auditable basis for machine-checked mathematics.

Key points

  • The Metamath language uses only a handful of keywords: $c, $v, $d, $f, $e, $a, $p, plus scoping braces. Extensions include typesetting ($t), extra metadata ($j), file inclusion, and a compressed proof format.
  • The main database, set.mm, builds mathematics on propositional calculus, predicate calculus with equality (based on Tarski's S2 plus auxiliary axioms) and ZFC set theory. It reaches a worked formal proof that 2 + 2 = 4.
  • The Metamath program offers commands for reading, verifying, interactively constructing and improving proofs, for example prove, unify, improve and verify proof. It can also export LaTeX and HTML.
  • The appendices give a formal description of Metamath as a formal system, the MIU system as a toy example, and an EBNF grammar of the language.
  • The 2nd edition (2019, Lulu Press, ISBN 978-0-359-70223-7) by Norman Megill, revised by David A. Wheeler, is released into the public domain under CC0 1.0. The only exceptions are the short third-party quotations it contains.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Fields, topics and concepts

📚 Shelf 1The field of science this work belongs to (OpenAlex fields).Mathematics · 233 works

🧭 Topics 1Research subjects and languages the work is about.Reasoning · 1,948 works

Cite

Cite as Norman Megill and David A. Wheeler. 2019. Metamath: A Computer Language for Mathematical Proofs. Lulu Press (2nd ed.).

The paper itself, not this page. BibTeX from the library's record of the work.

@inproceedings{megill2019metamath,
  title = {{Metamath: A Computer Language for Mathematical Proofs}},
  author = {Norman Megill and David A. Wheeler},
  booktitle = {Lulu Press (2nd ed.)},
  year = {2019},
  url = {https://us.metamath.org/}
}

References

77 references, 1 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Donald J. Albers and G. L. Alexanderson, editors. Mathematical People. Contemporary Books, Inc., Chicago, 1985. [QA28.M37]. find
  2. Alan Ross Anderson and Nuel D. Belnap. Entailment, volume 1. Princeton University Press, Princeton, 1975. [QA9.A634 1975 v.1]. find
  3. John D. Barrow. Theories of Everything: The Quest for Ultimate Explanation. Oxford University Press, Oxford, 1991. [Q175.B225]. find
  4. H. Behnke, F. Backmann, K. Fladt, and W. Süss, editors. Fundamentals of Mathematics, volume I. The MIT Press, Cambridge, Massachusetts, 1974. [QA37.2.B413]. find
  5. J. L. Bell and M. Machover. A Course in Mathematical Logic. North-Holland, Amsterdam, 1977. [QA9.B3953]. find
  6. Andrea Blass. The interaction between category theory and set theory. In John Walter Gray, editor, Mathematical Applications of Category Theory (Proceedings of the Special Session on Mathematical Applications Category Theory, 89th Annual Meeting of the American Mathematical Society, held in Denver,… find
  7. W. W. Bledsoe and D. W. Loveland, editors. Automated Theorem Proving: After 25 Years (Proceedings of the Special Session on Automatic Theorem Proving, 89th Annual Meeting of the American Mathematical Society, held in Denver, Colorado January 5–9, 1983), Providence, Rhode Island, 1983. American Mathe… find
  8. George S. Boolos and Richard C. Jeffrey. Computability and Logic. Cambridge University Press, Cambridge, third edition, 1989. [QA9.59.B66 1989]. find
  9. John Campbell. Programmer’s Progress. White Star Software, Box 51623, Palo Alto, CA 94303, 1991. find
  10. Mario Carneiro. Conversion of HOL light proofs into metamath. CoRR, abs/1412.8091, 2014. — [arXiv:1412.8091](https://arxiv.org/abs/1412.8091) find
  11. Mario Carneiro. Natural deductions in the metamath proof language. 2014. find
  12. Shang-Ching Chou. Proving elementary geometry theorems using Wu’s algorithm. In W. W. Bledsoe and D. W. Loveland, editors, Automated Theorem Proving: After 25 Years (Proceedings of the Special Session on Automatic Theorem Proving, 89th Annual Meeting of the American Mathematical Society, held in Den… find
  13. Richard Courant and Herbert Robbins. Topology. In James R. Newman, editor, The World of Mathematics, Volume One, pages 573–590. Simon and Schuster, New York, 1956. [QA3.W67 1988]. find
  14. Haskell B. Curry. Foundations of Mathematical Logic. Dover Publications, Inc., New York, 1977. [QA9.C976 1977]. find
  15. Philip J. Davis and Reuben Hersh. The Mathematical Experience. Birkhäuser Boston, Boston, 1981. [QA8.4.D37 1982]. find
  16. Richard de Millo, Richard Lipton, and Alan Perlis. Social processes and proofs of theorems and programs. In Thomas Tymoczko, editor, New Directions in the Philosophy of Mathematics, pages 267–285. Birkhäuser Boston, Inc., Boston, 1986. [QA8.6.N48 1986]. find
  17. Robert E. Edwards. A Formal Background to Mathematics. Springer-Verlag, New York, 1979. [QA37.2.E38 v.1a]. find
  18. Herbert B. Enderton. Elements of Set Theory. Academic Press, Inc., San Diego, 1977. [QA248.E5]. find
  19. R. L. Goodstein. Development of Mathematical Logic. Springer-Verlag New York Inc., New York, 1971. [QA9.G6554]. find
  20. Michael Guillen. Bridges to Infinity. Jeremy P. Tarcher, Inc., Los Angeles, 1983. [QA93.G8]. find
  21. Alan G. Hamilton. Logic for Mathematicians. Cambridge University Press, Cambridge, revised edition, 1988. [QA9.H298]. find
  22. John Robert Harrison. Metatheory and reflection in theorem proving: A survey and critique. Technical Report CRC-053. SRI Cambridge, Millers Yard, Cambridge, UK, 1995. Available on the Web as http:-//www.cl.cam.ac.uk/users/jrh/papers/reflect.html. find
  23. John Robert Harrison. Theorem proving with the real numbers. Technical Report 408, University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge, CB2 3QG, UK, 1996. Author’s PhD thesis, available on the Web at http://www.cl.cam.ac.uk-/users/jrh/papers/thesis.html. ↗
  24. Horst Herrlich and George E. Strecker. Category Theory: An Introduction. Allyn and Bacon Inc., Boston, 1973. [QA169.H567]. find
  25. J. Roger Hindley and David Meredith. Principal type-schemes and condensed detachment. The Journal of Symbolic Logic, 55:90–105, 1990. [QA.J87]. find
  26. Douglas R. Hofstadter. Gödel, Escher, Bach. Basic Books, Inc., New York, 1979. [QA9.H63 1980]. find
  27. Andrzej Indrzejczak. Natural deduction, hybrid systems and modal logic. Trends in Logic, 30, 2010. find
  28. D. Kalish and R. Montague. On Tarski’s formalization of predicate logic with identity. Archiv für Mathematische Logik und Grundlagenforschung, 7:81–101, 1965. [QA.A673]. find
  29. J. A. Kalman. Condensed detachment as a rule of inference. Studia Logica, 42(4):443–451, 1983. [B18.P6.S933]. find
  30. Morris Kline. Mathematical Thought from Ancient to Modern Times. Oxford University Press, New York, 1972. [QA21.K516 1990 v.3]. find
  31. Morris Kline. Mathematics, The Loss of Certainty. Oxford University Press, New York, 1980. [QA21.K525]. find
  32. Oliver Knill. Some fundamental theorems in mathematics. 2018. find
  33. Edna E. Kramer. The Nature and Growth of Modern Mathematics. Princeton University Press, Princeton, New Jersey, 1981. [QA93.K89 1981]. find
  34. Daniel Clemente Laboreo. Introduction to natural deduction. 2014. find
  35. Edmund Landau. Foundations of Analysis. Chelsea Publishing Company, New York, second edition, 1960. [QA241.L2541 1960]. find
  36. Hugues Leblanc. On Meyer and Lambert’s quantificational calculus FQ. The Journal of Symbolic Logic, 33:275–280, 1968. [QA.J87]. find
  37. Czeslaw Lejewski. On implicational definitions. Studia Logica, 8:189–208, 1958. [B18.P6.S933]. find
  38. Azriel Levy. Basic Set Theory. Dover Publications, Mineola, NY, 2002. find
  39. Angelo Margaris. First Order Mathematical Logic. Blaisdell Publishing Company, Waltham, Massachusetts, 1967. [QA9.M327]. find
  40. Adrian R. D. Mathias. A term of length 4,523,659,424,929. Synthese, 133:75–86, 2002. [Q.S993]. find
  41. Norman D. Megill. A finitely axiomatized formalization of predicate calculus with equality. Notre Dame Journal of Formal Logic, 36:435–453, 1995. [QA.N914]. find
  42. Norman D. Megill and Martin W. Bunder. Weaker D-complete logics. Journal of the IGPL, 4:215–225, 1996. Available on the Web at http:-//www.mpi-sb.mpg.de/igpl/Journal/V4-2/\#Megill. find
  43. Elliott Mendelson. Introduction to Mathematical Logic. D. Van Nostrand Company, Inc., New York, second edition, 1979. [QA9.M537 1979]. find
  44. C. A. Meredith. Single axioms for the systems (C,N), (C,O) and (A,N) of the two-valued propositional calculus. The Journal of Computing Systems, 3:155–164, 1953. find
  45. David Meredith. In memoriam Carew Arthur Meredith (1904-1976). Notre Dame Journal of Formal Logic, 18:513–516, 1977. [QA.N914]. find
  46. J. Donald Monk. Substitutionless predicate logic with identity. Archiv für Mathematische Logik und Grundlagenforschung, 7:103–121, 1965. find
  47. A. W. Moore. The Infinite. Routledge, New York, 1989. [BD411.M59]. find
  48. James R. Munkres. Topology: A First Course. Prentice-Hall, Inc., Englewood Cliffs, New Jersey, 1975. [QA611.M82]. find
  49. E. Z. Nemesszeghy and E. A. Nemesszeghy. On strongly creative definitions: A reply to V. F. Rickey. Logique et Analyse (N. S.), 20:111–115, 1977. [BC.L832]. find
  50. I. Németi. Algebraizations of quantifier logics, an overview. Version 11.4, preprint, Mathematical Institute, Budapest, 1994. A shortened version without proofs appeared in “Algebraizations of quantifier logics, an introductory overview,” Studia Logica, 50:485–569, 1991 [B18.P6.S933]. find
  51. M. Pavičić. A new axiomatization of unified quantum logic. International Journal of Theoretical Physics, 31:1753 –1766, 1992. [QC.I626]. find
  52. Roger Penrose. The Emperor’s New Mind. Oxford University Press, New York, 1989. [Q335.P415]. find
  53. Ivars Peterson. The Mathematical Tourist. W. H. Freeman and Company, New York, 1988. [QA93.P475]. find
  54. Jeremy George Peterson. An automatic theorem prover for substitution and detachment systems. Notre Dame Journal of Formal Logic, 19:119– 122, 1978. [QA.N914]. find
  55. Willard Van Orman Quine. Set Theory and Its Logic. The Belknap Press of Harvard University Press, Cambridge, Massachusetts, revised edition, 1969. [QA248.Q7 1969]. find
  56. J. A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the Association for Computing Machinery, 12:23– 41, 1965. find
  57. T. Thacher Robinson. Independence of two nice sets of axioms for the propositional calculus. The Journal of Symbolic Logic, 33:265–270, 1968. [QA.J87]. find
  58. Rudy Rucker. Infinity and the Mind: The Science and Philosophy of the Infinite. Bantam Books, Inc., New York, 1982. [QA9.R79 1982]. find
  59. Bertrand Russell. Recent work on the principles of mathematics. International Monthly, 4:84, 1901. find
  60. Bertrand Russell. Mysticism and Logic, and Other Essays. Barnes & Noble Books, Totowa, New Jersey, 1981. [B1649.R963.M9 1981]. find
  61. Eric Schmidt. Reductions in norman megill’s axiom system for complex numbers. 2012. find
  62. Joseph R. Shoenfield. Mathematical Logic. Addison-Wesley Publishing Company, Inc., Reading, Massachusetts, 1967. [QA9.S52]. find
  63. Daniel Solow. How to Read and Do Proofs: An Introduction to Mathematical Thought Process. John Wiley & Sons, New York, 1982. [QA9.S577]. find
  64. Harold M. Stark. An Introduction to Number Theory. Markham Publishing Company, Chicago, 1970. [QA241.S72 1978]. find
  65. E. R. Swart. The philosophical implications of the four-color problem. American Mathematical Monthly, 87:697–707, November 1980. [QA.A5125]. find
  66. George G. Szpiro. Poincaré’s Prize: The Hundred-Year Quest to Solve One of Math’s Greatest Puzzles. Penguin Books Ltd, London, 2007. [QA43.S985 2007]. find
  67. Gaisi Takeuti and Wilson M. Zaring. Introduction to Axiomatic Set Theory. Springer-Verlag New York Inc., New York, second edition, 1982. [QA248.T136 1982]. find
  68. Alfred Tarski. What is elementary geometry. In Leon Henkin, Patrick Suppes, and Alfred Tarski, editors, The Axiomatic Method, with Special Reference to Geometry and Physics (Proceedings of an International Symposium held at the University of California, Berkeley, December 26, 1957 — January 4, 1958)… find
  69. Alfred Tarski. A simplified formalization of predicate logic with identity. Archiv für Mathematische Logik und Grundlagenforschung, 7:61–79, 1965. [QA.A673]. find
  70. Thomas Tymoczko, editor. New Directions in the Philosophy of Mathematics. Birkhäuser Boston, Inc., Boston, 1986. [QA8.6.N48 1986]. find
  71. Hao Wang. Theory and practice in mathematics. In Thomas Tymoczko, editor, New Directions in the Philosophy of Mathematics, pages 129–152. Birkhäuser Boston, Inc., Boston, 1986. [QA8.6.N48 1986]. find
  72. Daniel Whalen. Holophrasm: a neural automated theorem prover for higher-order logic. CoRR, abs/1608.02644, 2016.
  73. Alfred North Whitehead. An Introduction to Mathematics, 1911. find
  74. Alfred North Whitehead and Bertrand Russell. Principia Mathematica. Cambridge University Press, Cambridge, second edition, 1927. (3 vols.) [QA9.W592 1927]. find
  75. Freek Wiedijk. The qed manifesto revisited. 2007. find
  76. Stephen Wolfram. Mathematica: A System for Doing Mathematics by Computer. Addison-Wesley Publishing Co., Redwood City, California, second edition, 1991. [QA76.95.W65 1991]. find
  77. Larry Wos, Ross Overbeek, Ewing Lusk, and Jim Boyle. Automated Reasoning: Introduction and Applications. McGraw-Hill, Inc., New York, second edition, 1992. [QA76.9.A96.A93 1992]. Index find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/megill-2019-metamath-computer-language-mathematical-proofs/