Georges Gonthier is a RESEARCHER in the Programming Principles and Tools Group.

Programming Principles and Tools Group's home page.

His 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. The latter subject inspired his latest work, 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 a description of the notations and the proof command language that were used to write the proof.