MosaikHub Magazine

Portrait Georges Gonthier, « hacker » de théorèmes

lundi 3 novembre 2014

« Avec son côté “hacker” tout en étant brillant en mathématiques, Georges Gonthier était la personne idéale pour défricher ce domaine de la vérification informatique des théorèmes mathématiques », raconte Gérard Berry, professeur au Collège de France qui a été son directeur de thèse. L’intéressé se définit plutôt comme un informaticien, mais reconnaît que ses connaissances poussées en mathématiques ont été plus qu’utiles. L’enjeu : vérifier la justesse des résultats mathématiques, ce que les mathématiciens écrivent sous la forme de théorèmes.

S’il est facile de faire cette vérification pour des théorèmes dont la démonstration est courte, comme celui de Pythagore, cela devient plus compliqué lorsque les démonstrations occupent des centaines de pages de raisonnement. C’est ce qu’est parvenu à faire Georges Gonthier à deux reprises, d’abord en 2004 avec le théorème des quatre couleurs – qui stipule que quatre couleurs suffisent pour colorier toute carte sans que deux régions de même teinte se touchent – et fin 2012 avec le théorème de l’ordre impair, un résultat majeur de la théorie des groupes.

« DÉCRIRE DES PROGRAMMES INFORMATIQUES QUI S’EXÉCUTENT SIMULTANÉMENT »

La vérification de preuves mathématiques est devenue son domaine de recherche principal, alors que ce n’était au départ qu’un projet annexe pour ce chercheur qui partage son temps entre le laboratoire de recherche Microsoft à Cambridge et le laboratoire commun Microsoft-Inria, à Palaiseau (Essonne), dont il a participé à ...

L’accès à la totalité de l’article est protégé


Accueil | Contact | Plan du site | |

Creative Commons License

Promouvoir & Vulgariser la Technologie