|
COLLOQUIA PATAVINA |
|
Proof engineering, from the Four Color to the Odd Order Theorem
Georges Gonthier (Microsoft Research)Thirty five years ago computers
made a dramatic debut in mathematics with the famous proof of
the Four Color 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.