Interview de Sébastien Gouëzel, prix Brin 2019

Pouvez-vous nous décrire les travaux récompensés par ce prix ?

Prenez un dé à 6 faces, et lancez-le beaucoup de fois. Même si vous essayez de faire le même lancer à chaque fois, les résultats auront l’air aléatoires, avec tous les nombres entre 1 et 6 qui sortiront dans les mêmes proportions. Et pourtant, il n’y a rien d’aléatoire dans le mouvement du dé, qui est régi par les lois (déterministes) de la physique ! Cela s’explique par le fait que le mouvement est suffisamment complexe pour amplifier les petites différences inévitables dans les conditions initiales pour produire un hasard apparent. On dit que ce système est chaotique.

Une large part de mon travail est d’étudier ce phénomène de manière précise : dans quelle mesure les résultats d’un système déterministe peuvent-ils ressembler à un phénomène aléatoire ? Il s’agit d’étudier des systèmes concrets (souvent beaucoup plus simples que les systèmes physiques pertinents, trop complexes à comprendre mathématiquement - on parle de modèles jouet), et de donner des outils mathématiques généraux pour quantifier la vitesse à laquelle ces systèmes mélangent. La motivation que j’ai donnée est d’origine physique mais, de manière étonnante, de nombreuses transformations abstraites, d’origine géométrique ou algébrique, présentent aussi ce type de comportement. Ces travaux de dynamique ont donc aussi des applications internes aux mathématiques dans des directions inattendues.

Vous êtes directeur de recherche au CNRS. Comment décririez-vous votre métier à une jeune lycéenne passionnée de mathématiques ?

Je fais un métier très particulier, dans lequel je suis libre de choisir sur quels problèmes travailler car personne n’est mieux placé que moi pour savoir dans mon domaine quelles sont les questions intéressantes. Il y a tout d’abord une partie administrative, de gestion et d’organisation, sur laquelle je ne m’étendrai pas mais qui n’est pas négligeable.

La partie intéressante, mathématique, se partage en trois. Il y a tout d’abord la lecture et l’écriture d’articles. C’est dans les articles qu’on trouve les détails techniques des preuves et que la pérennité de la connaissance mathématique est assurée : si quelqu’un a besoin d’utiliser un de mes théorèmes dans 50 ans, il faut qu’il puisse tout comprendre sans avoir besoin de me passer un coup de fil. Mais la transmission des résultats récents se fait beaucoup plus par des interactions directes entre mathématiciennes et mathématiciens, dans des conférences ou dans des discussions informelles : les mathématiciennes et mathématiciens sont aussi des animaux sociaux ! Des collaborations fructueuses peuvent ainsi se nouer entre des personnes avec des domaines d’expertise un peu différents, qui peuvent allier leurs forces pour comprendre des problèmes qui ne leur seraient pas accessibles individuellement.

Enfin, il y a une partie plus solitaire, où il s’agit de réfléchir à un problème pour essayer de le résoudre. Parfois, les outils classiques suffisent, mais souvent il faut inventer de nouvelles idées, ce qui est difficile : cela demande du temps et de l’obstination (voire même un côté un peu obsessionnel). Quand on a l’impression d’être sur le point de résoudre un problème qui nous intéresse depuis longtemps, on ne peut s’empêcher de le ressasser et le retourner dans sa tête en permanence, pendant des jours et des jours ou des semaines et des semaines, jusqu’à avoir l’illumination (ou pas, d’ailleurs : il faut aussi savoir gérer la frustration). Il arrive souvent que mes enfants me voient immobile et apparemment en train de rêver devant une fenêtre, pendant de longues minutes, et m’interpellent alors avec un sourire en coin : ils savent très bien que j’étais en train de faire des maths.

Sur votre site internet, votre mentionnez votre intérêt pour les « preuves assistées par ordinateur ». Pouvez-vous nous décrire ce qu’est une preuve assistée par ordinateur et ce que ce concept apporte à vos recherches ?

Le monde universitaire actuel est très concurrentiel, comme le symbolise bien l’adage « publier ou périr ». La communauté est donc poussée à écrire de plus en plus d’articles, très vite, sans forcément bien les vérifier. De plus, nos résultats sont de plus en plus complexes et sophistiqués, et il n’est pas rare de voir des articles extrêmement techniques de 100 pages voire 200 pages que personne n’a lus soigneusement, mais qui sont réutilisés ensuite. Il y a d’ailleurs eu récemment plusieurs polémiques entre équipes mathématiques travaillant sur des sujets proches, chaque équipe affirmant que les résultats de l’autre étaient incorrects, et la complexité des arguments étant telle qu’il était très difficile pour la communauté de trancher. Cette situation ne me semble pas satisfaisante, et j’ai l’impression que les assistants de preuve pourraient être une solution.

Pour les mathématiciennes et mathématiciens, les objets que nous manipulons sont tout à fait concrets et familiers, et les théorèmes et démonstrations sont un discours logique qui traduisent le comportement de ces objets. Mais d’un point de vue très terre à terre, une démonstration est juste une suite de symboles qui obéit à certaines règles simples, qu’on peut expliquer à un ordinateur. Les assistants de preuve sont des programmes informatiques qui réalisent cet objectif. On devrait d’ailleurs plutôt les appeler vérificateurs de preuve : l’utilisateur ou l’utilisatrice rentre une démonstration dans une syntaxe appropriée (qui ressemble un peu à un langage informatique), et le programme vérifie que le passage d’une ligne à la suivante respecte les règles logiques et utilise juste des résultats déjà démontrés. On pourrait ainsi en théorie formaliser toutes les mathématiques, même si la tâche est colossale : ces programmes, pourtant très sophistiqués, ont besoin de preuves beaucoup plus détaillées que ce qui suffit à convaincre un mathématicien ou une mathématicienne, capable avec son expérience et son bagage technique de comprendre des raisonnements assez rapides. En contrepartie, on peut croire une preuve formalisée dans un assistant de preuve avec un degré de confiance beaucoup plus élevé que par les processus d’évaluation classique.Pour l’instant, l’utilisation des assistants de preuve par les mathématiciennes et mathématiciens est tout à fait marginale. Personnellement, ce processus m’a déjà permis de trouver des erreurs dans des papiers d’autres mathématiciens (et dans l’un des miens !), qui se sont toujours avérées être réparables : les mathématiciennes et mathématiciens fonctionnent d’abord avec une excellente intuition de ce qui est vrai grâce à leur familiarité avec les objets qu’ils manipulent. J’espère que dans un horizon de 10 ou 20 ans les assistants de preuve deviendront des outils du quotidien, et permettront de garantir que tous nos résultats sont corrects.