Proof Engineering, from the Four Colour to the Odd Order Theorem

Thirty-five years ago, computers made a dramatic debut in mathematics with the famous proof of the Four Colour Theorem by Appel and Haken. Their role has been expanding recently, from computational devices to tools that can tackle deduction and proofs too complex for (most) human minds, such as the Kepler conjecture or the Classification of Finite Simple Groups. These new “machine” proofs entail fundamental changes in the practice of mathematics: a shift from craftsmanship, where each argument is a tribute to the ingenuity of the mathematician that perfected it, to a form of engineering where proofs are created more systematically. In addition to formal definitions and theorems, mathematical theories also contain clever, context-sensitive notations, usage conventions, and proof methods. To mechanize advanced mathematical results it is essential to capture these more informal elements, replacing informal and flexible usage conventions with rigorous interfaces, and exercise apprenticeship with precise algorithms. This can be difficult, requiring an array of techniques closer to software engineering than formal logic, but it is essential to obtaining formal proofs of graduate-level mathematics, and can give new insight as well. In this talk, we will give several examples of such empirical formal mathematics that we have encountered in the process of mechanizing a large corpus of Combinatorics and Algebra required by the proofs of the Four Colour and Odd Order Theorem.