Opinion: The Mechanization of Mathematics

searched for a word containing the initial letters of the words "formal," "proof," and "Kepler," and settled on "Flyspeck," which means "to scrutinize, or examine carefully."The project was completed in August of 2014. 1 In May of 2016, three computer scientists, Marijn Heule, Oliver Kullmann, and Victor Marek, announced a solution to an open problem posed by Ronald Graham.Graham had asked whether it is possible to color the positive integers red and blue in such a way that there are no monochromatic Pythagorean triples, that is, no monochromatic triple a, b, c satisfying a 2 + b 2 = c 2 .Heule, Kullmann, and Marek determined that it is possible to color the integers from 1 to 7,824 in such a way (see Figure 1), but that there is no coloring of the integers from 1 to 7,825 with this property.They obtained this result by designing, for each n, a propositional formula that describes a coloring of 1, . . ., n with no monochromatic triple.They then used a propositional satisfiability solver, together with heuristics tailored to the particular problem, to search for satisfying assignments for specific values of n.For n = 7,824, the search was successful, yielding an explicit coloring of the corresponding range of integers.For the negative result, however, it is riskier to take the software's failure to find a coloring as an ironclad proof that there isn't one.Instead, Heule, Kullmann, and Marek developed an efficient format to encode a proof that the search was indeed exhaustive, providing a certificate that could be checked by independent means.The resulting The Mechanization of Mathematics