Research

Headband Research

Laboratoires.Ecoles, Collège et Formation doctorales 

Stratégie. Séminaires, colloques. Sciences et société

Réseaux et pôles d'excellence. Investissements d'avenir (Labex)

Creative Commons license Le génie mathématique, du théorème des quatre couleurs à la classification des groupes [Oct. 4, 2012]

 Summary

George Gonthier (Microsoft & INRIA) / LIG

Voilà plus de trente ans que l’informatique et les ordinateurs ont fait irruption dans les mathématiques, avec la célèbre preuve du théorème des quatre couleurs par Appel et Haken. Leur rôle s’est amplifié récemment, car ils permettent maintenant de maîtriser non plus seulement des calculs, mais aussi des raisonnements dont la complexité dépasse les capacités de l’esprit humain (ou du moins, de la plupart), comme la preuve de la conjecture de Kepler ou la classification des groupes simples finis. Cependant, ces preuves "machine" exigent un changement profond de la pratique des mathématiques : un passage de l’artisanat, où chaque argument est un tribut à l’ingéniosité du mathématicien qui l’a ciselé, à une forme d’ingénierie, où les preuves sont construites à l’aide de techniques plus systématiques. On substitue ainsi des interface rigoureuses aux conventions d’usage malléables, et des algorithmes précis à l’apprentissage de méthodes par des exercices. Parvenir à codifier ainsi une part de l’état de l’art mathématique assez importante pour permettre de coder des preuves intéressantes, représente un défi considérable ; nous montrerons comment nous avons réussi à le relever, en complétant la preuve du théorème de Feit-Thompson, la première étape majeure de la classification des groupes finis.

Tags: keynote lig

 Infos

 Downloads

Video file(s):

Audio file:

 Embed/Share

 Options
Check the box to autoplay the video.
Check the box to loop the video.
Check the box to indicate the beginning of playing desired.
 Embed in a web page
 Share the link
qrcode
Comments have been disabled for this video.