The Four-Color Theorem and the Aesthetics of Computational Proof

This article uses the 1976 proof of the four-color theorem—the first instance of a major mathematical problem to be solved with the assistance of a computer—as a lens through which to explore current debates in the digital humanities. Critics of computational text analysis often represent it as imposing an alien, quantitative, or mathematical methodology onto qualitative literary material; and yet, the computational proof of the four-color theorem has also been notoriously controversial amongst mathematicians, many of whom reject the very idea of computer-assisted proof. This article explores two overarching sets of questions that have fundamentally shaped the reception of computational methods in both fields—the first about whether arguments based on computational analysis meet the standards of proof we have come to expect in either mathematics or literary criticism; the second about the role of aesthetics in our assessment of an argument’s validity. Attending to the mathematical debates that emerged out of the four-color theorem can help humanities scholars better articulate concerns about the surveyability of computational evidence and the reliability of experimental as opposed to deductive methodologies, while also prompting us to take seriously the connection between the aesthetic and epistemic components of our arguments. Conversely, the study of history, philosophy, and aesthetics can help contextualize changing mathematical ideas about the nature of proof.