Tweet
Un projet collaboratif a été lancé pour apprendre l’énoncé à un ordinateur. Un défi colossal, alors que celui-ci s’appuie sur des concepts profonds en théorie des nombres, en géométrie et en analyse.
Par Samia Hanachi
Une page de l’ouvrage de Pierre de Fermat « Varia opera mathematica », édition de 1679. SCIENCE PHOTO LIBRARY/AKG-IMAGES
Le dernier théorème de Fermat n’a pas fini de donner du fil à retordre aux mathématiciens. Il aura fallu plus de trois siècles pour trouver sa démonstration, il faudra plusieurs années pour la faire comprendre par un ordinateur. C’est l’objectif d’un projet collaboratif et open source d’envergure, financé à hauteur de 930 000 livres sterling (environ 1,1 million d’euros), entre 2024 et 2029.
L’énoncé, découvert dans les archives du mathématicien Pierre de Fermat (1601-1665) après sa mort, est pourtant simple : si a, b et c sont des nombres naturels non nuls, alors l’équation an + bn = cn n’a pas de solution lorsque n est strictement supérieur à 2. Dans ses notes, Fermat prétendait que les marges de son cahier étaient « trop étroites » pour contenir la démonstration et ce n’est donc qu’en 1994 que le Britannique Andrew Wiles en viendra à bout.
Kevin Buzzard, mathématicien à l’Imperial College de Londres et coordinateur du projet, connaît bien cette histoire. A l’époque, il est doctorant et son directeur de thèse, Richard Taylor, s’envole pour les Etats-Unis afin d’aider Wiles à finaliser sa preuve. « Je me suis retrouvé sans encadrant, mais c’était pour la bonne cause, plaisante-t-il. Ce théorème a toujours occupé une place centrale dans ma vie. »
Lire aussi l’archive (1993) | Article réservé à nos abonnés Le théorème de Fermat : le triomphe de l’inaccessible
Pour l’expliquer à l’ordinateur, « il faut une armée », insiste le mathématicien. Les démonstrations sont habituellement rédigées pour un public expert, qui partage un socle de connaissances communes. Elles sautent des étapes classiques ou considérées comme triviales, font référence à des raisonnements analogues dans d’autres preuves… « Avec une machine, cela ne marche pas. Elle est stupide, elle a besoin qu’on lui explique tout, développe Sébastien Gouëzel, directeur de recherche CNRS en mathématiques à l’université Rennes-I. C’est un peu comme construire une cathédrale. Si vous voulez poser la flèche, il faut avoir mis toutes les pierres au-dessous. »
Un exercice mental particulier
Le défi est d’autant plus colossal que la démonstration du dernier théorème de Fermat est connue pour sa complexité. « Il faut avoir fait une thèse en théorie des nombres pour la comprendre, j’aurais du mal à l’expliquer à un mathématicien en dehors de mon champ de recherche », explique Riccardo Brasca, chercheur à l’Institut de mathématiques de Jussieu-Paris-Rive gauche, qui participe au projet.
La preuve fait le lien entre l’équation de l’énoncé et un objet mathématique appelé « courbe elliptique ». Elle consiste à montrer que, si l’équation a des solutions, alors il y aurait une courbe elliptique aux propriétés étranges, dont l’existence est impossible. Elle s’appuie sur des concepts profonds en théorie des nombres, en géométrie et en analyse.
« A ma connaissance, aucun autre projet similaire n’a nécessité des prérequis aussi larges et poussés. Etablir une feuille de route détaillée est même un défi en soi », insiste Andrew Yang, qui travaille dessus à temps plein dans le cadre de sa thèse à l’Imperial College de Londres.
Pour l’instant, une trentaine de personnes ont déposé des parties de code informatique sur la page GitHub créée pour l’occasion. Mais les contributeurs sont bien plus nombreux sur le forum des usagers de Lean, le logiciel utilisé. En fonction de leur expertise, ils apportent leur aide sur des questions mathématiques, informatiques… ou techniques. Car l’un des enjeux de la collaboration est de documenter clairement le plan et l’avancement du projet. L’outil LeanBlueprint, développé par Patrick Massot, professeur au laboratoire de mathématiques d’Orsay (Essonne), permet cela.
« 14 h 15, 14 h 45, 14 h 50… il y a tout le temps des messages », commente Riccardo Brasca, face au fil de discussion sur son écran, dans son bureau parisien. Il consacre la moitié de son temps de recherche à évaluer les contributions et à les intégrer dans la bibliothèque de Lean, Mathlib. « A ce stade, la principale difficulté concerne la masse de travail. Ce théorème utilise une quantité de maths déraisonnable, donc il y a beaucoup de choses à formaliser, même si elles ne sont, pour l’instant, pas très compliquées. »
Portrait de Pierre de Fermat (1601-1665) en frontispice de son ouvrage « Varia opera mathematica », édition de 1679. BRITISH LIBRARY/KHARBINE/LA COLLECTION
Traduire les mathématiques pour une machine est un exercice mental particulier. Cela nécessite d’être astucieux, de trouver, parmi les différents chemins pour démontrer un résultat, le plus simple à expliquer à l’ordinateur. « On ressort de ces expériences avec une manière un peu différente de penser, les concepts sont mieux organisés dans le cerveau », décrit Riccardo Brasca.
« Sécuriser les démonstrations »
Mais, hormis pour la beauté de l’exercice, à quoi cela sert-il ? « Chaque mathématicien vous donnera une réponse différente, déclare Sébastien Gouëzel. Personnellement, je suis convaincu de l’intérêt de ces projets pour sécuriser les démonstrations. J’ai vu trop d’articles faux ou à moitié faux pour être satisfait du système actuel. » Une fois les démonstrations écrites dans un langage de programmation comme Lean, Isabelle ou Coq (bientôt renommé Rocq), elles peuvent être vérifiées automatiquement. Ces « assistants de preuve » existent depuis la fin des années 1960, mais cela fait peu de temps que les mathématiciens s’en emparent. Un pas de géant a été franchi en 2021, lorsque la communauté Lean a permis de valider et même de simplifier une démonstration de Peter Scholze, médaillé Fields, dont il doutait lui-même.
Cette incertitude n’existe pas pour le théorème de Fermat : « Il a tellement été utilisé que, s’il était faux, on s’en serait rendu compte depuis longtemps », explique Riccardo Brasca. Mais cela n’empêche pas que des imprécisions puissent être repérées sur le chemin, comme l’a constaté Antoine Chambert-Loir, professeur à l’Institut de mathématiques de Jussieu-Paris-Rive gauche. En s’intéressant à un bout de théorie utilisé dans la preuve du théorème de Fermat, écrit uniquement en français, dans les années 1960, il s’est rendu compte qu’un des arguments mobilisés était ambigu et méritait d’être réécrit.
C’est aussi arrivé à David Angdinata, doctorant de Kevin Buzzard, qui travaille sur une autre partie de la démonstration. « Dans la littérature, tout le monde partait du principe qu’il existait une certaine preuve algébrique sans que personne se soit vraiment plongé dans les détails. Ils s’avèrent beaucoup plus compliqués que prévu », relate-t-il.
Ce projet permettra, par ailleurs, d’enrichir la bibliothèque Mathlib avec des objets mathématiques complexes, qui permettront de vérifier d’autres démonstrations particulièrement pointues à l’avenir, notamment en théorie des nombres.
Quand on le questionne sur l’intérêt du projet, Kevin Buzzard, plus romantique, évoque d’abord sa longue histoire d’amour avec le théorème. Puis la joie de collaborer en équipe : « Ma compagne est chirurgienne et publie des articles avec des dizaines de personnes. En maths, c’est très rare d’être plus de deux. J’avais envie moi aussi de travailler avec plein de gens ! »