What Progress Made in Automated Verification of Mathematical Proofs?

Question

The problem was that these [automated proof verification] systems were extraordinarily cumbersome. Checking a single theorem could require a decade of work, because the computer essentially had to be taught all of the mathematics a proof was built on, in agonizing, inhuman detail. Ordinary mathematicians intent on expanding the borders of the field could not possibly devote that kind of effort to checking their proofs.

Somehow, computers and humans needed to be taught to think alike.

Dr. Voevodsky developed a stunningly bold plan for how to do so: He reformulated mathematics from its very foundation, giving it a new “constitution.” [...] Mathematics so reformulated would be far friendlier to computers and allow mathematicians to talk to computers in a language that was much closer to how mathematicians ordinarily think.

OBITUARIES|Vladimir Voevodsky, Revolutionary Mathematician, Dies at 51, NYT Oct. 6, 2017

To what extent has this new "constitution" (homotopy type theory?) been successful in making the automated verification of mathematical proofs easier?

Answer 1

My understanding of the situation (which is no doubt over-simplified and may well be inaccurate) is that when Voevodsky started looking for systems for machine-checking mathematics, he started using Coq and became interested in the semantics the underlying Calculus of Inductive Constructions (CIC). (I have no idea to what extent Voevodsky explored other mechanized proof assistants/frameworks such as HOL or Mizar.) The upshot is that he discovered that CIC could be given semantics in structures that are used in abstract homotopy theory and further those semantics suggested new axioms, particularly the Univalence Axiom, to make the fit tighter. This led to a theory, homotopy type theory (HoTT), that is conjectured to be the internal language of $(\infty,1)$-toposes. The theory of $\infty$-categories was and still is an area of intense and active interest, and this provides a clean description of a large and important class of such $\infty$-categories. Even better, it does this by connecting to systems which have been studied and implemented for decades.

It's useful to know the context and a bit of the history of the Calculus of Inductive Constructions. The first thing to note is that CIC already is a different foundations of mathematics based on dependent type theory and specifically Martin-Löf type theory. It also already "changes the meaning of the equals sign" and the fact that it is most naturally a constructive system has significant consequences to the logic overall. (It is consistent to add axioms to CIC to make it classical, so it's not an anti-classical framework.) Indeed, the behavior and meaning of equality in these systems has been a puzzle since the beginning.

In a dependent type theory with inductive types, equality can be defined with an inductive data type. In Coq, it looks like:

Inductive identity (A:Type) (a:A) : A -> Type :=
    identity_refl : identity a a.

Two values, x and y, of a type A are considered "equal" whenever there exists a value of identity A x y. A key division point in dependent type theories is whether or not this notion of equality should correspond to the implicit, built-in notion of equality that is used to check whether an expression is well-typed, called definitional equality. (The above notion is often called "propositional equality".) If I apply a function of type A -> B to a value of type C, I need to verify that A = C for that to be type correct, and in a dependently typed language that can be highly non-trivial involving arbitrarily large amounts of computation. The question is then: if I have a value of type identity A x y, i.e. if x and y are propositionally equal, should I be able to, for example, apply a value of type F x to a function of type F y -> Z? That is, should I be able to derive that x and y are definitionally equal? Systems that answer this affirmatively are called extensional type theories and equality in them behaves quite similarly to how it "normally" does. Systems that answer negatively are called intensional type theories and seem to be what the logic/math is suggesting. They also have meta-theoretic properties that are nice. Extensional type theories make definitional equality (and thus type checking) undecidable, while it is usually decidable in intensional type theories.

The story gets stranger. It turns out it's impossible to prove that given two proofs of propositional equality, i.e. two values p, q : identity A x y, they are propositionally equal. Formally, the type forall p q : identity A x y, identity (identity A x y) p q may or may not be inhabited depending on A, x, and y. This was demonstrated in Hofmann and Streicher's The Groupoid Interpretation of Type Theory after many failed attempts to prove the above statement (for all A, x, and y) which is called the Uniqueness of Identity Proofs (UIP). My impression, pre-HoTT, is that many viewed this as a nuisance or, at best, as a necessary evil. The goal of these systems (especially the implementations) was not explore new frontiers of mathematics, but to provide a practical framework for doing "normal" mathematics (or computer science, as many working on these things were computer scientists more than mathematicians). The failure of UIP and related failures such as the failure of function extensionality was (and is) quite obnoxious. Agda incorporates Axiom K, a variation of UIP, but function extensionality still fails (though it is often also postulated) and UIP is not the same thing as having an extensional notion of equality; you still have to manually "transport" terms along identity which adds a large amount of complexity that just doesn't exist in extensional systems, let alone informal mathematics.

All this was happening before Voevodsky even started looking at Coq. What Voevodsky found was that all this obnoxious extra work that needed to be done was being done to allow for the case of non-trivial values of identity types (indeed, this is what the Hofmann and Streicher groupoid interpretation illustrates) but there's no way to actually talk about/make any of these non-trivial values. UIP and Axiom K are basically statements to the effect that there are no non-trivial values, but Voevodsky, inspired by abstract homotopy theory, went the other way. He introduced a way to refer to some non-trivial values of identity types via the Univalence Axiom. The punchy, slogan form (which is actually fairly accurate) is that the type of identities between two types A and B is equivalent to the type of equivalences between A and B. More formally, equiv (identity Type A B) (equiv A B) or in nicer syntax: $$(A\equiv_{\mathsf{Type}} B)\simeq(A\simeq B)$$ where equiv/$\simeq$ is roughly (the internal view of) "isomorphism", i.e. $A\simeq B$ if there are functions $f : A \to B$ and $g : B \to A$ such that $f\circ g \equiv id$ and $g \circ f \equiv id$. There's a technical detail that you want to avoid having multiple proofs of $\simeq$ so it needs to be stated a bit more carefully than that, but that's essentially what it's saying. Univalence thus does "change the meaning of the equals sign" even for intensional type theory, though it's a bit closer to "revealing" the meaning as opposed to "changing" it.

One nice consequence of this is that univalence implies function extensionality. While it doesn't eliminate the obnoxious busy-work that intensional type theory often requires, we start getting something for doing it. (Or at least it's clear that it is not for no reason, and the limitations cease being arbitrary and inscrutable.) More philosophically, this formalizes a principle that is completely ubiquitous in informal mathematics but technically invalid (particularly with regards to set-theoretic foundations); namely, the identification of equivalent things. This can be viewed as a formalization of the typically informal principle of equivalence of category theory, but, for a much more simple and concrete example consider the integers. One way to define the integers is as the set of equivalence classes (or a quotient type) of pairs of natural numbers. Alternatively, one could consider the subset $\{-,+\}\times\mathbb N \setminus (-, 0)$. You can easily imagine many other possible constructions. Nevertheless, mathematician virtually never bother specifying which construction they are using when they use the integers, but it is not the case that everything that is true for one construction of the integers is true for another. In Homotopy Type Theory (i.e. intuitionistic type theory [with inductive types] plus the univalence axioms [and nowadays higher inductive types]), it is the case. This is typically what people are referring to when they say HoTT, in particular, captures intuitions common in mathematical practice. Type theory in general also seems to capture many aspects of mathematical practice better than set theory, e.g. it was already the case in type theory that a statement like $7\in\pi$ would be nonsense. Indeed, this is crucial for univalence to be useful. The price of this in HoTT is that the notion of equality is more complex.

Since univalence, the notion of a higher inductive type (HIT) has arisen which is another way to add non-trivial values to identity types. These provide a different perspective on constructions built on the notion of quotienting which has been a weak area of intensional type theory. With these, in addition to rationalizing and simplifying pre-existing type constructors such as squash types, it's also possible to simply, compactly, and abstractly describe topological constructions such as topological circles, fundamental groupoids and loop spaces, and suspensions. For example, the circle type might be defined something like:

Inductive (circle : Type) :=
  | base : circle
  | loop : base ~~> base.

This is a direct declaration of what the circle is that captures everything of (abstract) homotopical relevance, but doesn't cloud it with extra data that we're just going to have to ignore/mod out anyway. This leads to new forms of proofs of homotopical facts, and certainly a new perspective. It also doesn't hurt that essentially overnight it gave homotopy theory mature mechanized proof assistants. There are deeper philosophical consequences of essentially building (abstract) homotopical structure into the logic itself, for example how it interacts with physics.

That last link describes the situation (circa 2012) as being similar to the dot-com bubble. It's clear something big has happened but what exactly should be done with it is less clear. It's certainly a long way from being standard material in an introduction to homotopy; however, being a tool for homotopy is not the sole or arguably even the primary goal. There is still a decent amount of theory to work out and infrastructure to be built including new proof assistants, such as RedPRL, that more directly incorporate features inspired by HoTT. Moving back from the specific question, there is also a social aspect to this pushing toward machine-verified proofs. In addition to Voevodsky's call for the adoption of mechanized proof assistants, the work on HoTT has to a large extent proceeded from formal (as in machine-checked) proofs with informal renditions following. For example, much of the Homotopy Type Theory book is an "informalization" of results that had formal, machine-checked proofs. This is a unique situation. Nevertheless, this is a bit of an orthogonal concern, and my impression is that some are annoyed the inordinate focus on this aspect. You certainly don't need to use a proof assistant to study HoTT.