vdash: What is Formal Math?	vdash Formal Math Wiki Roadmap Future
	The development of mathematics toward greater precision has led, as is well known, to the formalization of large tracts of it, so that one can prove any theorem using nothing but a few mechanical rules. — Kurt Gödel, "On Formally Undecidable Propositions of Principia Mathematica and Related Systems I", 1931 (via The QED Manifesto)   Introduction Formalized mathematics consists of mathematical theorems and proofs stated in a formal language, with enough detail that a computer program (called a proof assistant) can mechanically verify all of the steps, thereby certifying correctness. In the case of some large complicated proofs, formalization can add to our certainty that a result is correct. But even when we were already certain, formal math provides other benefits. Computers can directly parse formally stated theorems and their proofs, opening up new avenues in education, and new ways of visualizing and interacting with the mathematical corpus. Formal Proof — Theory and Practice, by John Harrison (Notices of the AMS), provides an excellent introduction. Other sources include Slawomir Kolodynski's Formalized Mathematics blog, How to (really) trust a mathematical proof (Science News, 2008), Proof and Beauty (The Economist, 2005), What in the name of Euclid is going on here? (Science, 2005), Does the proof stack up? (Nature, 2003), The QED Manifesto (1994), Formalized Mathematics (1996) and Handbook of Practical Logic and Automated Reasoning (to appear, 2009) by John Harrison, and Carlos Simpson's Computer theorem proving in math (2004) and, with Marco Maggesi, Information Technology implications for Mathematics.   Formalized Mathematics Proof assistants have steadily improved over the past several decades, and in recent years there have been increasingly large efforts towards verification of mathematical results using proof assistants. Freek Wiedijk has compiled a list of 100 theorems with formalizations in various proof assistants, which he discusses (Notices of the AMS). Jeremy Avigad formalized an elementary proof of the Prime Number Theorem in Isabelle/HOL, and John Harrison has recently formalized an analytic proof of the Prime Number Theorem in HOL Light. Flyspeck is an ongoing project to formalize Thomas Hales' proof of the Kepler Conjecture, which he discusses (Notices of the AMS). Georges Gonthier has formalized a proof of the Four-Color Theorem in Coq, which he also discusses (Notices of the AMS). He discovered "new and rather elegant nuggets of mathematics in the process", and notes: Perhaps this is the most promising aspect of formal proof: it is not merely a method to make absolutely sure we have not made a mistake in a proof, but also a tool that shows us and compels us to understand why a proof works. Jeremy Avigad, Edward Dean, and John Mumma have proposed a formal system for faithfully presenting the proofs in Euclid's Elements.   Zermelo-Fraenkel: Isabelle/ZF Most proof assistants suitable for formalizing mathematics are based upon either type theory (often via higher order logic) or set theory (on top of first-order logic). vdash is based on Isabelle/ZF, an implementation of first-order logic with the Zermelo-Fraenkel axioms of set theory. While there are some portions of mathematics that are most readily formalized in a higher-order logic, we believe that a coherent collection of all mathematics is most simply expressed in terms of set theory. Furthermore, the situations where using set theory currently takes more work will be less frequent as more math is formalized in ZF, or can be mitigated by modular definitions that abstract away some set-theoretic details. There is also the possibility that conservative extensions of set theory (e.g., ZF augmented by definitions and partial functions) may make some aspects of formalization easier, as Steve Kieffer, Jeremy Avigad, and Harvey Friedman have recently demonstrated. Other approaches to formalized ZF set theory include Mizar, a proof assistant with a set-theoretic language (which formalizes Tarski-Grothendieck — an extension of ZFC), Metamath, a library of proofs in ZFC by Norman Megill, David McAllester's language Ontic, Carlos Simpson's approaches with Coq, and Mike Gordon's work on combining ZF and HOL and on ZF in HOL and Isabelle with Sten Agerholm.   Declarative Proofs: Isabelle/Isar Many proof assistants are based on a procedural approach, wherein the user guides the proof assistant through various tactics in sequence. Declarative proofs consist of statements presented in deductive order, and are much closer to informal mathematical style. For vdash, it is essential that the proofs themselves are human-readable, and hence in a declarative style. For other purposes, it may be sufficient to build a library of procedural proof scripts along with natural-language glosses, but for vdash the proofs themselves must be easily understood by human readers (even if there is additional informal commentary in comments). Isar (shown at right) is a declarative mode for Isabelle, and is the formal language in which Isabelle/ZF proofs are expressed in vdash. Isar Reference Manual by Makarius Wenzel Isar Tutorial by Tobias Nipkow Isabelle/Isar — a generic framework for human-readable proof documents by Makarius Wenzel Practical Theorem Proving with Isabelle/Isar by Jeremy Siek There is also a Declarative Proof Language for Coq, a Mizar Mode for HOL and Mizar Light for HOL Light. Mizar proofs are always written in a declarative style.   Other Formalization Efforts Several interactive theorem proving communities collect contributions in their libraries and beyond, e.g., Isabelle: ZF Library, HOL Library, IsarMathLib, and The Archive of Formal Proofs Mizar: Mizar Mathematical Library, Journal of Formalized Mathematics, and Formalized Mathematics Coq: Standard Library, Contribs, and Hypertextual Electronic Library of Mathematics HOL Light: HOL Light Examples HOL 4: Libraries and Theories ProofPower: PPHOL, PPZed, and Examples Nuprl: Math Library PVS: NASA Langley Libraries ACL2: Books Metamath: Metamath Proof Explorer Freek Wiedijk has compiled and edited a comparison of the features and proof styles of The Seventeen Provers of the World.