SIAM News Blog
SIAM News

Not many SIAM lectures begin by “proving” that $$64=65$$. But that is how Thomas Hales of the University of Pittsburgh chose to open his talk at the 2018 SIAM Annual Meeting, which took place in Portland, Ore., this July. Hales, who is known for his leading role in computationally-based proofs of the Kepler conjecture, was delivering the I. E. Block Community Lecture — part of SIAM’s effort to raise awareness of the many applications of mathematics. The $$64=65$$ paradox was the first stop in a tour that took his audience from lighthearted paradoxes in the popular press to those that upset the foundations of mathematics a century ago, before returning them to present day and the current state of self-verifying systems.

The $$64=65$$ paradox is resolved by finding an easily overlooked area in the geometric argument offered in its support: an $$8 \times 8$$ rectangle cannot be chopped into triangles and trapezoids to form a $$5 \times 13$$ rectangle without leaving uncovered on its diagonal a thin sliver of parallelogram that has unit area. Hales observed that such paradoxes enjoyed great popularity during their “golden age” in the early 20th century. During this time, much more profound paradoxes were simultaneously shaking the foundations of mathematics.

One of the most familiar paradoxes may be the barber paradox, which presents the following scenario: In a certain village, a male barber shaves exactly those men who do not shave themselves. Does the barber shave himself? Mathematicians quickly recognize that the inherent contradiction—the barber can neither shave himself nor not shave himself—is proof that no such barber exists. Does the contradiction represent a tectonic threat or merely an amusement?

Figure 1. One strand of the foundational work arising from Russell’s paradox. Logicomix: An Epic Search for Truth, by Apostolos Doxiadis and Christos Papadimitriou, is published by Bloomsbury Publishing (RRP \$25) [1].
Despite its superficial resemblance to the innocent barber conundrum, Russell’s paradox is powerfully consequential. Devised by British mathematician and philosopher Bertrand Russell, it states: $$X$$ is the set of all sets that do not have themselves as members. Does $$X$$ have itself as a member? Following the logic that resolved the barber paradox, we immediately conclude that no such set can exist. Then we pause in consternation; what became of our ability to define any set we wanted?

This startling outcome toppled the work of German philosopher Gottlob Frege, a luminary of mathematical logic. In a 1962 Scientific American article entitled “Paradox” [3]—which Hales rightly recommended to his listeners as essential homework—logician W.V. Quine demonstrated the way in which Russell’s paradox compels us to give up the fundamental principle of the existence of sets.

Hales summarized this critical period with a frame from the graphic novel Logicomix—the second of his essential reading assignments—that depicts the construction of the logical foundations of mathematics. Russell appears in the panel, famously working on Principia Mathematica with Alfred North Whitehead (see Figure 1).

Ernst Zermelo used a different approach to resolve Russell’s paradox. He proposed a theory of sets that dodged the paradox by prohibiting sets that are too large, such as the set of all sets. Russell’s theory of types, in contast, forbade types that overlap; the barber paradox is grammatically unsound because barbers and customers are distinct types (see Figure 2). Hales observed that set theory offers a foundation for much of mathematics, while type theory establishes a foundation for computer science.

Figure 2. Two responses to Russell’s paradox. Figure courtesy of Thomas Hales.

The rush of ideas continued. Kurt Gödel’s incompleteness theorem appeared in 1931: every sufficiently powerful deductive system contains a sentence that is true if and only if it is unprovable in that system. David Hilbert’s 1928 decision problem, which asks if there exists an algorithm that can determine the universal validity of a given logical statement, received independent negative answers from both Alonzo Church and Alan Turing in 1936. Turing showed that the halting problem—which asks whether a program will run forever or eventually halt, given a description of that program and an input to it—reduces to Hilbert’s decision problem. He then solved the halting problem by what Hales called a “paradoxical construction — an algorithm that takes as input a data-encoding of itself.”

Ultimately, Alexander Grothendieck introduced his concept of universes to accommodate sets larger than those permitted by Zermelo’s formulation. Figure 3 offers a caricature of these universes. The nutshell in the top center recursively contains Hales’ cartoon universe. He lightheartedly suggested that Hamlet foresaw these mathematical constructions when declaiming, “I could be bounded in a nutshell, and count myself a king of infinite space.”

Figure 3. Thomas Hales’ caricature of a mathematical universe, enclosed recursively in the nutshell at the top center. Creative Commons and Google Images.
Hales followed this path of paradoxes to offer his audience a glimpse of the superstructure needed to support a proof assistant—a programming language capable of validating mathematical proofs—built within such a nutshell universe. His perspective was surely influenced by his 1998 submission of a computationally-based proof by exhaustion of Johannes Kepler’s sphere-packing conjecture to Annals of Mathematics. (In 1611, Kepler had conjectured that a face-centered arrangement of uniform spheres packs most efficiently into a given volume; the stack of oranges in the upper right corner of Figure 3 is an example.)

The challenges of verifying Hales’ and his co-author Samuel Ferguson’s work overwhelmed the volunteer referees before they could definitively accept its validity. “It is very unusual to have such a large set of reviewers (working) … over a three-year period,” one editor reported. “The reviewing process produced in these reviewers a strong degree of conviction of the essential correctness of this proof approach…” This was good news, but hardly the traditional unequivocal endorsement.

Another editor relayed the thinking of referee panel head Gábor Fejes Tóth, younger half of the Fejes Tóth father-son team that played important 20th-century roles in the Kepler saga. “Fejes Tóth thinks that this situation … is similar to the situation in experimental science,” the editor said. “Other scientists acting as referees can’t certify the correctness of an experiment, they can only subject the paper to consistency checks. [Fejes Tóth] thinks the mathematical community will have to get used to this state of affairs.”

Despite his eventual publication of papers describing both the mathematical and computational portions of his proof of Kepler’s conjecture, Hales pursued the possibility of a computer checking “every step of the proof back to the foundations of mathematics.” In 2017, he published—with 21 collaborators—a formal proof of the Kepler conjecture in Forum of Mathematics, Pi [2]. That effort, known as the Flyspeck project, used the proof assistants Isabelle and HOL Light.

HOL Light is the work of John Harrison; its kernel requires less than 500 lines of code. After Hales discovered a bug at an early stage, Harrison used the corrected proof assistant to confirm the absence of any others. Such proofs of self-consistency dodge Gödel’s incompleteness theorem by looking back in from a slightly larger universe. Self-verification then enables mutual verification within the ecosystem of a multitude of proof assistants. A verified self-compiling compiler is accessible through the CompCert project, and the proof assistant community is within sight of top-to-bottom verification tools — from high-level code down to machine language.

Finally, Hales addressed confidence — the elephant in the room. “Do I completely trust computers?” he asked. “No. Do I completely trust human referees? No. The technologies have reached the point where I trust them as much as I trust any technical tool.” Mathematics might indeed be on the threshold of a brave new world—if not universe—of formal validation.

Hales’ presentation—including the “proof” that  $$64=65$$—is available from SIAM either as slides with synchronized audio or a PDF of slides only.

The I. E. Block Community Lecture is given annually at the SIAM Annual Meeting. It honors the vision of I. Edward Block, the co-founder and former managing director of SIAM, by encouraging public appreciation of the excitement and vitality of science. The lectures are open to students, teachers, and members of the local community, as well as SIAM members, researchers, and practitioners in fields related to applied and computational mathematics.

References
[1] Dosiadix, A., & Papadimitriou, C.H. (2009). Logicomix: An Epic Search for Truth. New York, NY: Bloomsbury Publishing.
[2] Hales, T., Adams, M., Bauer, G., Dang, T.D., Harrison, J., Hoang, L.T., …, Zumkeller, R. (2017). A Formal Proof of the Kepler Conjecture. Forum of Math., Pi, 5, e2.
[3] Quine, W.V. (1962, April). Paradox. Sci. Amer., 206(4), 84-96.

Paul Davis is professor emeritus of mathematical sciences at Worcester Polytechnic Institute.