12 · Types and Proofs
Fourth hearing of Part II. The last three chapters asked what computation can do, how long it takes, and what it moves; this one asks what happens to the oldest philosophical prize — certainty — once proof itself becomes a checkable artifact.
What happens to certainty when proof becomes an artifact?
In 1976 Kenneth Appel and Wolfgang Haken proved the four-color theorem with the help of a computer program that checked close to fifteen hundred map configurations no human being would ever survey by hand — chapter 03 already sat with the shock that verdict caused: a proof too long for any mathematician to read start to finish. Nearly thirty years later Georges Gonthier closed a different case about the same theorem. His formalization, completed in the Coq proof assistant and published as "Formal Proof — The Four-Color Theorem" (Notices of the American Mathematical Society 55, 2008: 1382–1393), did not merely rerun Appel and Haken's argument; it re-derived the whole proof, combinatorics and case-checking alike, as a sequence of steps validated by a small trusted kernel that a single person can, in principle, audit line by line. The theorem that once symbolized proof outrunning human comprehension became, in Gonthier's hands, the theorem that showed comprehension could be replaced by something more exacting than any human reader: a machine that does not skim.
What makes Gonthier's kernel trustworthy is a correspondence discovered, not designed, twice over. Haskell Curry noticed in 1934 that the types assigned to combinators in combinatory logic could be read as axiom schemes of intuitionistic implicational logic, and in 1958 that a fragment of Hilbert-style proof systems coincided with a fragment of typed combinatory logic. William Howard made the analogy exact three decades later without knowing Curry's full history, circulating a manuscript in 1969 that was finally published as "The Formulae-as-Types Notion of Construction" in a 1980 festschrift for Curry edited by Jonathan Seldin and J. Roger Hindley. Howard showed that a proof, written in the natural-deduction style Gerhard Gentzen had introduced in 1935, and a program, written in the simply typed lambda calculus, are the same object viewed from two directions: a proposition is a type, a proof of it is a program of that type, and simplifying a proof — removing a detour — is executing the program. N. G. de Bruijn arrived at a version of the same idea independently at almost the same time, building it into his Automath system before either he or Howard knew of the other's work. Three researchers, working from logic, from combinators, and from an automated proof-checker, kept finding the identical seam — the strongest kind of evidence this book has for its own claim that philosophy and computing are one project rediscovered rather than two projects borrowed from each other.
The correspondence gave a century-old heresy its revenge. L. E. J. Brouwer's 1908 paper "The Unreliability of the Logical Principles" rejected the law of excluded middle — the claim that every statement is either true or false — for mathematics whose objects are mental constructions rather than mind-independent facts, building on the intuitionistic program he had opened in his 1907 dissertation. For most of the twentieth century this looked like a minority taste, a scruple most working mathematicians could safely ignore. Curry–Howard explains why it stopped being optional inside a proof assistant: a constructive proof that something exists must, under the correspondence, be a program that builds the thing, while a classical proof by contradiction — assume no such object exists, derive a contradiction, conclude one does — corresponds to no program at all, because it never says how to build anything. Coq, Agda, and Lean are, at their foundations, implementations of intuitionistic type theory not out of philosophical loyalty to Brouwer but because only the constructive fragment hands back code you can run. Intuitionism became load-bearing engineering exactly at the point where it stopped being asked to defend itself philosophically.
Once that machinery existed, mathematics started handing it its hardest, longest proofs. Thomas Hales completed a proof of the Kepler conjecture — that no packing of equal spheres is denser than the familiar grocer's stack — in 1998, but the 250-page argument, part conventional and part computer-assisted, took twelve referees four years and left them only 99 percent confident it was correct. Hales responded in 2003 by launching the Flyspeck project to re-derive every step inside HOL Light and Isabelle; the formalization was completed in 2014, checked and independently rechecked that year, and published as "A Formal Proof of the Kepler Conjecture" (Forum of Mathematics, Pi, 2017). Flyspeck's tens of thousands of lemmas rest on a kernel small enough for a handful of people to inspect completely, in place of twelve referees who could only sample a proof too long to read whole. Lean's mathlib, a continuously growing, community-verified library built on the same foundations, now formalizes results across the whole of mathematics as they are proved, turning "has this been checked" into a question with a machine-checkable answer rather than a matter of reputation.
Vladimir Voevodsky pushed the foundations themselves one step further. Homotopy Type Theory: Univalent Foundations of Mathematics — the collective volume written by the Institute for Advanced Study program he led, published in 2013 — proposed reading types not as bare sets but as spaces, and proofs of equality between elements as paths between points — under Voevodsky's univalence axiom, structures that are isomorphic can be treated as identical, which gives mathematics's oldest and most abused word, "equal," a precise, checkable meaning it had never quite had before.
None of this delivers the certainty Hilbert wanted in 1930. A proof assistant's guarantee is only as strong as its kernel, and the kernel rests on a compiler, which rests on hardware, which can fail — the same regress Wittgenstein pressed against any rule that claims to interpret itself, and the same one chapter 03 raised as a Gettier problem for sensors and pipelines. What Curry–Howard delivers instead is certainty re-engineered as a budget: instead of trusting a 250-page argument and twelve tired referees, trust a kernel of a few thousand lines, state exactly what would have to fail for the proof to be wrong, and let that be the whole of the remaining doubt. Philosophy wanted proof to end an argument once and for all; computation's counteroffer is a proof that tells you precisely how small the argument left over actually is.
Connections
Chapter 01 introduces Curry–Howard as the logic chapter's treaty between the two disciplines; this chapter completes it. Chapter 03 is where the four-color theorem first caused its epistemological shock — this chapter is its answer. Chapter 09 supplies the incompleteness results that proof assistants must live inside rather than escape. Chapter 11's Kolmogorov complexity measures the length of a proof the way this chapter measures its trustworthiness.
Open questions
If a kernel can be made small enough for one person to audit, has the regress of trusting the verifier actually been stopped, or only shortened to a link short enough to overlook? Does univalence settle what "the same structure" means in mathematics generally, or only inside type theory's own house? And now that Lean's mathlib checks new results as they are proved, does mathematical knowledge still need the human community of referees at all, or only the community that decides which theorems are worth proving in the first place?
Go deeper
- Jean-Yves Girard, Yves Lafont, and Paul Taylor, Proofs and Types, Cambridge Tracts in Theoretical Computer Science 7 (Cambridge: Cambridge University Press, 1989) — free edition at paultaylor.eu/stable/prot.pdf.
- William Howard, "The Formulae-as-Types Notion of Construction," in To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, ed. J. P. Seldin and J. R. Hindley (New York: Academic Press, 1980), 479–490; Georges Gonthier, "Formal Proof — The Four-Color Theorem," Notices of the American Mathematical Society 55 (2008): 1382–1393 — ams.org/notices/200811/tx081101382p.pdf.
- Stanford Encyclopedia of Philosophy, "Intuitionism in the Philosophy of Mathematics" — plato.stanford.edu/entries/intuitionism.