Colloquia Patavina: Proof engineering, from the Four Color to the Odd Order Theorem

Martedi' 8 Gennaio 2013 - Georges Gonthier


Martedi' 8 Gennaio 2013 alle ore 16:00 in aula 1A150 della Torre Archimede, Georges Gonthier (Microsoft Research) terra' una conferenza della serie Colloquia Patavina.

La Commissione Colloquia
C. Bonotto, M.A. Garuti, M. Pavon, F. Rossi

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.

-Breve biografia
Georges Gonthier's research interests include programming language design and semantics, concurrency theory and its application to security, and methods and tools for the formal verification of computer programs. One of his achievements on the latter subject is a fully checked formal proof of the famous Four Colour Theorem, using the Coq proof assistant developed at INRIA, the French Institut National de Recherche en Informatique et Automatique (this was work in collaboration with Benjamin Werner of INRIA).

Mathematically inclined readers may consult a paper describing the mathematics of the formalization. Users of the Coq system, or brave souls wishing to delve into the actual Coq Proof of the Four Color Theorem, might also be interested in description of the notations and the proof command language that were used to write the proof.

Download Colloquia Patavina