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, and by extension of general mathematics. His recent research has focused on the latter, and the development of tools, methods and theories that make it possible to describe, process and verify research-level mathematics - including rigorous proofs.
One of his early achievements in this area 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). See also this paper describing the mathematical details of the formalization.
This work was the starting point of the Mathematical Components project at the MSR-Inria Joint Centre, which he has led since 2006. The Mathematical Components team continues to develop the Ssreflect proof scripting language, which has used to formalize the Odd Order Theorem, one of the key results in the Classification of finite simple groups, and the irrationality of zeta(3), a special case of the Riemann hypothesis.