|vdash: What is Formal Math?|
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)
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.
Other sources include
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.
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:
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
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.
Several interactive theorem proving communities collect contributions in their libraries and beyond, e.g.,
Freek Wiedijk has compiled and edited a comparison of the features and proof styles of The Seventeen Provers of the World.