Le théorème de Fermat et les ordinateurs
[\latexpage]
L’énoncé de ce théorème est la suivante :
Pour $n>2$, il n’existe pas des entiers naturels non triviaux $a$, $b$ et $c$ tels que :
$$ a^n + b^n = c^n$$
Ce théorème a été démontré en 1994 par le mathématicien Britannique Andrew Wiles. Toutefois, une équipe de chercheurs tente de l' »expliquer » aux ordinateurs selon un article du journal « le monde ».
En fait, le projet tente plutôt d’expliquer la démonstration à l’ordinateur en détaillant toutes ses étapes. Ce processus permet notamment de s’assurer sue toutes les opposables de la démonstration sont correctes. La difficulté du projet tient au fait que, malgré la simplicité de l’énoncé du problème, la démonstration fait appel à des théories mathématiques complexes.
Voici un extrait de cet article.
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 (voir plus haut l’énoncé).
Dans ses notes, Fermat prétendait que les marges étaient très é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’impérial College de Londres et coordinateur du projet, connaît bien cette histoire. À l’époque, il est doctorant et son directeur de thèse, Richard 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. Cé théorème a toujours occupé une place centrale dans ma vie. » 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, chercbeue en 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 Andew 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 çréé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 questionsm athématiques, informatiques… ou techniques. Car l’enjeu de la collaboration est de documenter clairement le plan et l’avancement du projet. L’outil LeanBlue-print, développé par Patrick Massot, professeur au laboratoire de mathématiques d’Orsay (Essonne), permet cela.
«14h15, 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.
Share on Facebook
Post on X
Follow us
