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)

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

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

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.

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.

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.