Feit, Thompson et Gonthier

Le théorème de Feit-Thomson qui traite de la classification des groupes finis simples a été démontré par Walter Feit et John Griggs Thompson in 1963. Il dit (ne me demandez pas de détail) que chaque groupe fini d'ordre impair est résoluble. Georges Gonthier et son équipe du labo INRIA-Microsoft ont achevé en Septembre sa preuve formelle en utilisant le système Coq développé à l'INRIA. Bravo!

Polémique hier au café au LSV:

• C'est un truc techniquement super mais les mathématiciens s'en foutent.
• Ils s'en foutent peut-être mais cela va changer profondément les mathématiques.
• Pas le moins du monde... 

Tout ce que je vais écrire est purement spéculatif et discutable. Je sais que de nombreux collègues mathématiciens hurleraient en le lisant. Mais comme nous sommes entre nous... 

Développer une preuve mathématique est quelque chose de purement artisanal, souvent impliquant seulement un crayon et une feuille de papier. On peut imaginer l'arrivée d'outils qui aideront les mathématiciens en vérifiant leurs hypothèses, en proposant des pistes, en développant des preuves formelles. Le mathématicien serait libéré de la partie fastidieuse des démonstrations. On sort de l'artisanat.

Développer une preuve mathématique est quelque chose de purement individuel (le plus souvent). On peut imaginer des collaborations entre des groupes de mathématiciens autour d'outils informatiques qui leurs permettraient d'additionner leurs talents, leurs efforts.

Bien sûr, tout ce que je dis s'applique aussi aux preuves de programme. C'est finalement un peu la même chose.

Il est énormément plus complexe de découvrir une preuve que de la vérifier. Les ordinateurs font mieux que nous dans la vérification. J'ose le sacrilège. Seront-ils un jour meilleurs que nos meilleurs mathématiciens pour démontrer des théorèmes? Et il nous resterait quoi? Peiner à comprendre leurs preuves? Proposer des théorèmes?