Pourquoi la preuve du grand théorème de Fermat n'a pas besoin d'être améliorée

Au fil des décennies, depuis la preuve historique du grand théorème de Fermat, plusieurs idées ont émergé sur la manière de le rendre encore plus fiable. Cependant, ces tentatives reflètent une profonde méconnaissance de ce qui rend les preuves importantes.

Le 23 juin marque le 25e anniversaire de l'annonce d' Andrew Wiles , qui a excité tout le monde, dans laquelle il a annoncé la réception d'une preuve du grand théorème de Fermat , le problème le plus célèbre en mathématiques à l'âge de 350 ans. L'histoire entourant les preuves de Wiles - il a travaillé secrètement sur ce projet pendant sept ans, le manque de preuves qui est apparu après l'annonce de juin, une solution élégante publiée un an plus tard dans un travail conjoint écrit par Wiles avec son ancien élève Richard Taylor , qui a reçu le titre de chevalier en 2000 - est entré dans les annales des légendes mathématiques.

Après la percée de Wiles, on peut souvent entendre des spéculations sur l'avènement d'une nouvelle «ère d'or» en mathématiques, en particulier en théorie des nombres - le domaine auquel appartient le théorème de Fermat. Les méthodes présentées par Wiles et Taylor font aujourd'hui partie de la boîte à outils des experts en théorie des nombres qui considèrent que l'histoire du Grand Théorème est close. Mais cette histoire a touché non seulement les spécialistes de la théorie des nombres.

Les événements de 2017 me l'ont soudain rappelé, lorsque, dans l'intervalle de plusieurs jours, deux logiciens qui ont fait des rapports sur deux continents différents ont montré des moyens d'améliorer la preuve du théorème - et ont dit à quel point leurs collègues étaient surpris lorsque les experts en théorie des nombres ne se sont pas montrés leurs idées sont sans intérêt.

Les logiciens ont exprimé ces idées dans les langues de leurs spécialités respectives - la théorie des ensembles et l'informatique théorique. Les propositions qu'ils ont faites étaient intrinsèquement vraies et, peut-être un jour, poseraient-elles de nouvelles questions, non moins intéressantes que celles de Fermat. Cependant, il est immédiatement devenu clair pour moi que ces questions ne sont pas liées aux spécialistes de la théorie des nombres, et toute autre hypothèse reflète une profonde méconnaissance de la nature de la preuve de Wiles et des objectifs de la théorie des nombres en général.

Les racines de ce malentendu peuvent être trouvées dans la simplicité de l'énoncé du théorème, qui est responsable de la plupart de son attractivité: si n est un entier positif supérieur à 2, alors il est impossible de trouver trois tels nombres positifs, a, b et c, tels que:

$$

$$a ^ n + b ^ n = c ^ n$$

Cela contraste vivement avec le cas où n est 2: toute personne qui a étudié la géométrie euclidienne se souviendra que 3 ² + 4 ² = 5 ² , que 5 ² + 12 ² = 13 ² , etc. (cette liste est interminable). Au cours des derniers siècles, les mathématiciens ont essayé d'expliquer l'existence d'un tel contraste et, à chaque fois, ils ont échoué, laissant derrière eux de toutes nouvelles branches des mathématiques. Parmi ces branches, il y a de grands domaines de la théorie moderne des nombres, attirés par Wiles pour sa solution réussie, ainsi que de nombreuses idées fondamentales dans chaque partie de la science touchée par les mathématiciens. Et pourtant, personne avant Wiles ne pouvait prouver la prétention de Fermat.

Les informaticiens se sont récemment montrés ravis d'apprendre les progrès réalisés dans la confirmation automatique des preuves - une tentative ambitieuse de mettre en pratique l'approche formaliste des mathématiques. Pour les formalistes, la preuve mathématique est une liste de déclarations qui satisfont à des restrictions strictes:

1. Les déclarations en tête de liste devraient inclure des idées généralement acceptées. Dans une interprétation rigoureuse, cela ne comprend que les axiomes de la théorie des ensembles formels, généralement issus du système formel connu sous le nom de ZFC (système de Zermelo-Frenkel avec l'axiome de choix). Ceci est complètement impraticable, donc nous permettons également l'inclusion de théorèmes déjà prouvés - par exemple, le Grand Théorème pour le cas n = 4, que Fermat lui-même a prouvé au 17ème siècle.
2. Chaque relevé subséquent doit être obtenu en appliquant les règles de déduction logique aux relevés précédents.
3. Enfin, le théorème prouvé devrait être à la dernière place de la liste.

La logique mathématique a été développée dans l'espoir de placer les mathématiques sur une base solide - comme un système axiomatique exempt de contradictions, capable de raisonner sans glisser dans l'incohérence. Bien que le travail de Kurt Gödel ait montré l'irréalisabilité de ce rêve, de nombreux philosophes des mathématiques, ainsi que certains logiciens (une minorité petite mais active, selon les experts en théorie des ensembles) se réfèrent toujours à ZFC et aux exigences mentionnées comme une sorte de constitution des mathématiques.

Cependant, les mathématiciens n'écrivent jamais de preuves de cette manière. Une analyse logique des preuves de Wiles indique de nombreuses étapes qui ne prennent pas en compte ZFC, avec un potentiel de scandale: si les mathématiciens élaborent des règles sans vérifier la constitutionnalité, comment savent-ils qu'ils signifient tous la même chose?

La vérification automatique des preuves semble offrir une solution à ce problème. Il s'agit de reformuler les preuves par le biais d'un ensemble de déclarations distinctes, chacune étant écrite dans un langage cohérent que l'ordinateur peut lire, puis de confirmer la fidélité constitutionnelle de chaque étape. Cette méthode chronophage a été appliquée avec succès à de nombreuses épreuves longues et complexes, dont la plus célèbre est la preuve de l'hypothèse de Kepler sur l'emballage de sphères le plus dense faite par Thomas Hales. Tester les preuves de Wiles a longtemps été considéré comme l'un des principaux objectifs. Par conséquent, mon ami, un expert en informatique, était vraiment déçu que la recherche de «mathématiciens purs qui soutiennent catégoriquement l'utilisation d'outils automatiques dans la construction de leurs arguments», comme il l'a formulé, n'ait pas encore donné de résultats.


" Arithmétique " de l'édition Diophantus de 1670, dans laquelle la note notoire de Fermat est également incluse dans le texte principal. En traduction, il se lit comme suit: «Il est impossible qu'un cube soit la somme de deux cubes, pour le quatrième degré, il est impossible d'être la somme de deux quatrièmes degrés, ou, en général, pour tout nombre représentant un degré supérieur au second, il est impossible d'être la somme de deux des mêmes degrés. J'ai découvert des preuves vraiment merveilleuses de cette hypothèse, pour lesquelles ces champs sont trop étroits pour tenir. "

La première chose qui ne tient pas compte de cette déception est que les preuves de Wiles, bien que complexes, ont une base simple qui est facile à expliquer à un public borné. Supposons que, contrairement à la déclaration de Fermat, il existe trois entiers positifs a, b, c tels que

(A) a ^p + b ^p = c ^p

pour un nombre premier impair p (et il suffit de considérer uniquement les nombres premiers). En 1985, Gerhard Frey a montré que a, b et c peuvent être réorganisés en

(B) une nouvelle équation appelée "courbe elliptique"

avec des propriétés que tout le monde pensait impossibles. Plus précisément, on sait depuis longtemps comment exprimer cette courbe elliptique en termes de

(C) Représentation galoisienne

qui est un ensemble infini d'équations liées à la fois à la courbe elliptique et à l'autre par des règles claires.

Le lien entre ces étapes était bien connu en 1985. À ce moment-là, la plupart des experts en théorie des nombres étaient convaincus - bien qu'il n'y ait aucune preuve jusqu'à présent - que chaque représentation de Galois pouvait être attribuée, encore une fois, selon des règles claires,

(D) une fonction modulaire,

quelque chose comme une généralisation bidimensionnelle des fonctions sinus et cosinus familières de la trigonométrie.

Le lien final a été obtenu lorsque Ken Ribet a confirmé l'hypothèse de Jean-Pierre Seur selon laquelle les propriétés d'une fonction modulaire données par la forme de la courbe elliptique de Frey impliquent l'existence de

(E) une autre fonction modulaire de poids 2 et de niveau 2.

Cependant, de telles fonctions ne peuvent pas exister. Il n'existe donc ni fonction modulaire (D), ni représentation galoisienne (C), ni équation (B), ni solution (A).

Il ne restait plus qu'à trouver le chaînon manquant entre (C) et (D), que les mathématiciens appelaient l'hypothèse de modularité.

Ce lien a fait l'objet d'une recherche de sept ans sur Wiles. De notre point de vue actuel, il est difficile d'apprécier pleinement le courage de cette entreprise risquée. Vingt ans après que Yutaka Taniyama et Goro Shimura aient signalé pour la première fois la relation entre (B) et (D) à (C) dans les années 1950, les mathématiciens sont progressivement parvenus à la conclusion qu'il devait en être ainsi. Cet espoir a été exprimé dans un ouvrage très populaire d'André Weil, qui s'intègre idéalement dans le programme extrêmement influent de Langlands , du nom du mathématicien canadien Robert Langlands. Cette connexion était trop bonne pour ne pas être vraie. Cependant, l'hypothèse de modularité semblait totalement irréalisable. Les objets des types (C) et (D) étaient trop différents.

L'informaticien n'a pas expliqué si sa déception était due au fait qu'il n'était pas important pour la théorie des nombres que la preuve se limite à trouver le lien critique entre (C) et (D), ou qu'elle allait de (A) à (E). Je n'essaierai pas de le comprendre. Mais si les logiciens devaient seulement confirmer formellement la preuve publiée de la connexion entre (C) et (D), alors leurs attentes étaient trop élevées. Premièrement, Wiles s'est avéré un peu plus que suffisant pour que l'hypothèse de modularité complète la déduction «de (A) à (E)». L'hypothèse complète de la modularité a été établie plusieurs années plus tard par Christoph Broglie, Brian Conrad, Fred Diamond et Richard Taylor. Mais cela ne jette pas une ombre sur le travail de Wiles! Au contraire, le fait qu'un si grand nombre des meilleurs experts mondiaux de la théorie des nombres ait suivi les traces du travail de Wiles quelques mois seulement après son apparition parle de sa richesse.

Par exemple, un peu plus tard, à l'automne 2016, 10 mathématiciens se sont rencontrés à l'Institute for Advanced Studies de Princeton, New Jersey, et ont pu prouver l'existence d'une connexion entre les courbes elliptiques et les fonctions modulaires dans de nouvelles conditions. Ils ont tous utilisé des chemins différents pour comprendre la structure des preuves de Wiles, qui sont apparues lorsque certains d'entre eux étaient encore des enfants. Si on leur avait demandé de décrire cette preuve sous la forme d'une séquence de conclusions logiques, ils en auraient sans aucun doute publié 10 versions différentes. Chacun d'eux ressemblerait au chemin de (A) à (E) décrit ci-dessus, mais serait beaucoup plus détaillé.

Néanmoins - et cela est toujours négligé du point de vue philosophique des preuves - chacun de ces dix attribuerait la paternité de ses preuves à Wiles. Ils s'y référeraient de la même manière que les autres preuves qu'ils ont étudiées dans des articles explicatifs ou dans des cours de formation auxquels ils ont assisté ou enseigné. Et bien que chacun des dix aurait omis certains détails, en général, ils auraient tous raison.

Quelle est la preuve de Wiles si elle peut avoir autant d'options différentes? En philosophie mathématique, il est d'usage de traiter une preuve publiée comme une approximation d'une preuve formalisée idéale, qui peut en principe être vérifiée sur un ordinateur qui applique les règles d'un système formel. Les preuves idéales ne sont pas contaminées par quoi que ce soit en dehors du système formel - comme si chaque loi portait une marque confirmant sa justification constitutionnelle.

Mais cette approche contredit ce que les mathématiciens eux-mêmes disent de leurs preuves. Les mathématiciens n'utilisent pas de tests décisifs idéologiques ou philosophiques, mais je suis convaincu que la plupart de mes collègues seront d'accord avec Michael Francis Atiyah, qui a déclaré que la preuve "est le test final, mais pas la base de quoi que ce soit." Les preuves publiées ne sont clairement pas le fondement de quoi que ce soit.

Wiles et spécialistes de la théorie des nombres, affinant et développant ses idées, ne s'attendaient certainement pas à recevoir des offres de deux logiciens. Mais - contrairement à beaucoup de gens qui observent de loin la théorie des nombres - ils ont certainement compris qu'une preuve telle que celle publiée par Wiles ne devrait pas être traitée comme une sorte d'artefact en soi. Au contraire, la preuve de Wiles est le point de départ d'un dialogue ouvert trop insaisissable et vivant pour être limité à de sérieuses limites étrangères au sujet.