- Le travail de transcription de la preuve de FLT dans Lean est en cours depuis deux mois ; les définitions de R et T nécessaires au théorème « R=T » de Wiles ne sont pas encore terminées, mais un résultat d’algèbre commutative abstraite a déjà été démontré
- L’objectif n’est pas de reproduire à l’identique la preuve originale des années 1990, mais de construire dans Lean et mathlib une preuve généralisée et simplifiée à partir de travaux ultérieurs de Diamond/Fujiwara, Kisin, Taylor, Scholze et d’autres
- Lors de la formalisation de la cohomologie cristalline nécessaire à cette preuve moderne, un problème est apparu : un lemme clé de l’article de Roby de 1965, référence standard sur les structures à puissances divisées, semble faux
- Brian Conrad a retrouvé une preuve alternative dans l’annexe du livre de Berthelot-Ogus, et Arthur Ogus a aussi indiqué savoir corriger les erreurs de cette annexe, ce qui permet au projet de reprendre
- Ce cas montre le risque qu’il y a à faire reposer les détails des preuves mathématiques modernes sur la mémoire des experts et des savoirs implicites, et renforce les raisons pratiques d’enregistrer les preuves dans des systèmes formels
État actuel de la transcription de la preuve de FLT dans Lean
- Le travail visant à enseigner à un ordinateur la preuve du dernier théorème de Fermat (FLT) est en cours depuis deux mois
- Dans le théorème « R=T », cœur de la preuve de Wiles, définir ce que sont R et T dans Lean demande beaucoup de travail, et ces deux définitions ne sont pas encore terminées
- Le doctorant Andrew Yang a déjà démontré le résultat d’algèbre commutative abstraite nécessaire
- Il s’agit d’un résultat du type : « si des anneaux abstraits R et T satisfont plusieurs conditions techniques, alors ils sont égaux »
- Une version de travail est publiée sous forme de blueprint
- Le système utilisé est Lean avec la bibliothèque mathématique mathlib
- Les personnes ayant quelques connaissances de Lean et de théorie des nombres peuvent participer via les consignes de contribution, le tableau de bord du projet et les issues
Pourquoi ne pas simplement transcrire la preuve des années 1990
- Le projet ne formalise pas à l’identique la preuve de Wiles des années 1990
- Depuis, les travaux de Diamond/Fujiwara, Kisin, Taylor, Scholze et d’autres ont généralisé et simplifié la preuve
- L’objectif n’est pas seulement de démontrer FLT, mais de construire dans Lean des résultats plus généraux et plus puissants
- Si une révolution de l’IA mathématique se produit réellement et que Lean en devient un composant important, il peut être utile que les ordinateurs disposent des définitions centrales de la théorie moderne des nombres sous une forme exploitable
Les puissances divisées nécessaires pour la cohomologie cristalline
- La preuve qu’on cherche à formaliser utilise la cohomologie cristalline, absente de la preuve originale de Wiles
- Cette théorie a été développée à Paris dans les années 1960 et 1970, sur des idées de Grothendieck, avec des bases posées par Berthelot
- Les fonctions exponentielle et logarithme classiques sont essentielles pour comprendre la géométrie différentielle et la cohomologie de de Rham, mais elles ne fonctionnent pas telles quelles dans des contextes arithmétiques comme la caractéristique p
- Les structures à puissances divisées, développées notamment dans les articles de Roby dans les années 1960, jouent un rôle central pour construire des fonctions analogues utilisables en contexte arithmétique
- Pour enseigner la cohomologie cristalline à Lean, il faut d’abord formaliser les puissances divisées
Le problème mis au jour dans la littérature de Roby pendant le travail dans Lean
- Antoine Chambert-Loir et Maria Ines de Frutos Fernandez formalisaient dans Lean la théorie des puissances divisées
- Pendant l’été, Lean a mis en évidence un problème dans l’argumentation informelle de la littérature standard ; après vérification, un lemme clé dans le travail de Roby semblait faux
- Techniquement, l’article de Berthelot ne redéveloppe pas la théorie des puissances divisées depuis le début et s’appuie sur « Les algebres a puissances divisees » de Roby
- Cet article a été publié dans Bull Sci Math, 2ième série, 89, 1965, p. 75-91
- Le Lemme 8, p. 86, semble faux, et la manière de corriger la preuve n’était pas claire
- La preuve cite de travers un autre lemme figurant dans un article de Roby de 1963 dans Ann Sci ENS
- L’énoncé correct est
Gamma_A(M) tensor_A R = Gamma_R(M tensor_A R), mais une étape d’application omet un produit tensoriel
- Ce problème invalide la preuve de Roby selon laquelle l’algèbre à puissances divisées d’un module possède des puissances divisées, et bloque par conséquent la définition de l’anneau
A_cris
Une situation plus proche de « la preuve a un trou » que de « la théorie est fausse »
- Cela ne signifie pas que la cohomologie cristalline elle-même est substantiellement fausse
- Les grands théorèmes semblent toujours corrects, mais la preuve suivie par Antoine et Maria Ines était incomplète
- Roby, Grothendieck et Berthelot étant tous décédés, il n’était plus possible d’interroger directement les experts d’origine
- Plusieurs spécialistes estimaient que, même si un lemme intermédiaire est faux, la preuve des résultats principaux peut être réparée
- En formalisation, il ne suffit pas de penser que « cela devrait pouvoir se corriger » : il faut une preuve effectivement corrigée
Le détour rendu possible par l’annexe de Berthelot-Ogus
- Tadashi Tokieda a raconté cette histoire à Brian Conrad à Stanford, et Conrad a demandé ce que signifiait cette idée selon laquelle la cohomologie cristalline serait erronée
- Après avoir entendu les détails techniques, Conrad a reconnu que le problème semblait réel et s’est penché dessus
- Quelques heures plus tard, Conrad a signalé qu’une autre preuve du fait que l’algèbre universelle à puissances divisées d’un module possède des puissances divisées figure dans l’annexe du livre de Berthelot-Ogus sur la cohomologie cristalline
- Du point de vue de Conrad, cette approche semblait correcte, ce qui permettait de relancer la preuve
- Plus tard, lors d’un déjeuner avec Arthur Ogus à Berkeley, en lui racontant que cette annexe résolvait le problème, Ogus a répondu qu’elle contenait elle aussi plusieurs erreurs, mais qu’il savait comment les corriger
Pourquoi la littérature mathématique moderne a besoin de la formalisation
- Ce processus montre que la manière dont les humains documentent les mathématiques modernes n’est peut-être pas assez robuste
- De nombreux faits restent à l’état de « choses que les experts savent », sans être formulés précisément dans la littérature
- Même si les idées importantes sont assez solides pour résister à ce genre de choc, les détails effectifs des preuves peuvent ne pas se trouver là où l’on s’attend à les trouver
- En consignant correctement les mathématiques dans des systèmes formels, on peut réduire fortement le risque d’erreur
- Même pour les mathématiciens non formalistes, si l’on veut qu’une machine apprenne les raisonnements humains et fasse des mathématiques par elle-même, il faut d’abord lui enseigner ces raisonnements
- Maria Ines a présenté la formalisation des puissances divisées au séminaire Cambridge Formalization of Mathematics, et ces problèmes sont considérés comme résolus
- Le projet est revenu sur les rails, même si la littérature pourrait encore lui mettre des bâtons dans les roues
1 commentaires
Avis sur Hacker News
Cela me rappelle l’époque où, en doctorat, j’écrivais du code rapide pour aider mon directeur de thèse dans son approche calculatoire de la conjecture de Birch–Swinnerton-Dyer.
Lors d’un séminaire de théorie des nombres dans une ville voisine, on m’a demandé si je cherchais à renforcer les preuves en faveur de la conjecture ; j’ai répondu en souriant : « Non, j’aimerais plutôt trouver un contre-exemple », ce qui a mis les spécialistes très en colère.
La théorie des nombres est si ancienne et si profonde qu’écrire une thèse de doctorat dans ce domaine revient presque à devenir débutant ; on peut connaître les notations et les définitions sans atteindre l’intuition qui se trouve en dessous.
Donc la colère des spécialistes face à l’idée « d’espérer un contre-exemple » m’a laissé plus de curiosité que de crainte, et je me suis demandé ce qu’ils voyaient sans encore parvenir à le formuler.
Ce genre de progrès de la formalisation rend les mathématiques bien plus accessibles aux personnes pour qui la programmation est plus familière.
L’inquiétude liée au manque de formalité est légitime, mais je pense que la bonne réaction à cette inquiétude n’est pas l’évitement, mais la curiosité.
Si un bleu comme vous trouvait un contre-exemple avec des calculs grossiers et devenait célèbre du jour au lendemain, tous ces efforts et tout cet édifice pourraient s’effondrer ; je comprends qu’ils aient été furieux.
Si je devais donner un conseil de maths en master/doctorat à mon jeune moi, je lui dirais de consacrer au moins un quart du temps, pour chaque exercice non trivial du type « démontrer X », à la recherche de contre-exemples.
Dans les exercices, cela échouera 99 % du temps, mais votre compréhension du problème sera bien meilleure, et dans le 1 % restant vous aurez l’air d’un génie.
Quand on passe à la vraie recherche mathématique, les probabilités deviennent beaucoup plus favorables à une approche qui cherche d’abord les contre-exemples.
Quand j’étais étudiant, je me souviens qu’un ami m’a raconté qu’une personne venait de terminer le premier jour d’un séminaire et que tout le monde était excité à l’idée qu’il allait démontrer le dernier théorème de Fermat.
Cette personne était Andrew Wiles ; par la suite, après avoir corrigé pendant plusieurs mois un problème découvert avant publication, l’ensemble a finalement été publié.
Pour quelqu’un qui étudiait les mathématiques, c’était un événement incroyablement enthousiasmant ; du coup, voir l’expression « démonstration à l’ancienne des années 1990 » me donne vraiment l’impression d’être vieux.
La classe était presque entièrement composée de doctorants en maths, et je crois que je ne comprenais même pas 20 % du contenu.
J’ai aimé le passage où Lean a fait l’une de ces choses agaçantes qu’il fait parfois : il s’est plaint de la présentation, à la manière humaine, d’un raisonnement dans la littérature standard, et en y regardant de plus près, il y avait effectivement une lacune dans le raisonnement humain.
Blagues agacées mises à part, c’est remarquable, et je pense que Lean et les autres assistants de preuve deviendront des outils importants pour les mathématiques.
Le passage sur la mauvaise documentation des mathématiques modernes m’a fait penser à l’UI/UX/web design.
Un designer produit des maquettes, prototypes et flux d’interaction informels et imprécis, puis les transmet à un développeur ; celui-ci doit les formaliser en code et les expliquer précisément à la machine.
Dans ce processus, il découvre inévitablement des trous que la conception n’avait pas envisagés, comme des scénarios d’interaction ou des chemins de code, et parfois de gros défauts de conception apparaissent, que le développeur ou le designer doit combler.
Conception et développement sont des rôles différents qui exigent des façons de penser différentes, et la plupart des designers résistent fortement à l’idée de travailler et de penser comme des développeurs.
Après cet échec, nous avons appris qu’il est impossible de formaliser entièrement les mathématiques, ce qui pointe vers le problème fondamental des approches qui veulent faire des mathématiques avec l’IA.
Si ce sujet vous intéresse, il vaut mieux regarder le code réel.
Exemple : https://github.com/ImperialCollegeLondon/FLT/blob/main/FLT/M...
Le blueprint qui explique la structure d’ensemble du code vaut aussi le détour : https://imperialcollegelondon.github.io/FLT/blueprint/
Vu de l’extérieur, il est très intéressant de voir à quoi ressemble le code Lean et comment les gens y contribuent.
J’aime aussi le fait qu’il n’y ait pas besoin de tests unitaires. En un sens, l’énoncé final du théorème est le test unitaire.
Par exemple, de petits exemples et contre-exemples servant à vérifier qu’une définition n’est pas vide jouent ce rôle.
Du point de vue de quelqu’un qui a fait des mathématiques pures, le gros problème est que les mathématiciens fournissent rarement des démonstrations auto-suffisantes.
Ils n’ont aucune incitation à le faire, et il arrive même que les auteurs soient fiers d’« omettre les détails ».
Au final, si l’on veut une démonstration rigoureuse permettant de suivre toutes les étapes logiques, il faut qu’un spécialiste comble des lacunes qu’on ne trouve pas facilement dans la littérature.
Il faut parfois que cette personne écrive un livre expliquant tout pour que ce soit possible, et même cela ne suffit pas toujours.
Si l’on s’en tient à ce qui est consigné par écrit, une grande partie des mathématiques modernes repose sur des fondations instables.
Les articles de recherche en mathématiques sont écrits pour d’autres spécialistes du domaine, et il y a parfois trop peu de détails, ce dont on se plaint souvent lors de l’évaluation par les pairs.
Mais si l’on fournissait vraiment tous les détails, les articles seraient beaucoup plus longs.
Comme exemple accessible avec de solides bases de maths de lycée, on peut citer le problème consistant à prouver qu’il existe des constantes C, X > 0 telles que, pour tout réel x > X,
log(x^2 + 1) + sqrt(x) + x/exp(sqrt(4x + 3)) < Cx.Des énoncés de ce type apparaissent constamment en théorie analytique des nombres, et ils sont évidents pour les spécialistes ; dans les articles, ils sont donc presque toujours écrits sans démonstration.
Produire une démonstration complète et rigoureuse serait long et sans intérêt, et aucun spécialiste n’aurait envie de la lire.
Cette attitude a un coût de compromis, mais il semble rester gérable.
Cela ressemble à la troisième étape dont parle Tao : une intuition informée.
Il disait : « Si vous avez fait quelque chose 100 fois, vous pouvez dire “comme on l’observe facilement” et passer à la suite. »
Autrement dit, j’ai compris qu’il faudrait quelqu’un ayant une base de données dans la tête pour déterminer si les préconditions d’un théorème et la conclusion de la phrase suivante correspondent.
Ou bien je me demande s’il existe des mathématiques qu’on ne peut pas exprimer d’une manière évaluable par les vérificateurs de preuves actuels.
Ou encore, l’usage des vérificateurs de preuves n’est peut-être pas aussi répandu qu’on pourrait le croire. Cela ressemble à la place des langages à typage statique en programmation.
Autrement dit, s’il y a déjà eu un cas où une démonstration largement acceptée présentait une faille fatale à cause d’un passage balayé d’un geste de la main.
Si cela n’est jamais arrivé, on comprend aussi pourquoi l’attitude vis-à-vis de l’explicitation des détails est assez relâchée.
Je me suis toujours demandé si l’intuition selon laquelle « la cohomologie cristalline est tellement utilisée depuis les années 1970 que s’il y avait un problème, il serait apparu depuis longtemps » était vraiment correcte.
Est-il vraiment si impossible qu’un champ entier des mathématiques soit développé sur une démonstration défectueuse, puis que ce champ s’avère tout simplement faux ?
Il a vu de ses propres yeux un domaine s’effondrer à cause d’une erreur située dans le « premier lemme de la première page » d’un article fondateur.
Les premiers travaux sur UniMath, l’année spéciale à l’IAS, puis le livre HoTT ont contribué à porter le sujet de la formalisation des mathématiques à la place qu’il occupe aujourd’hui.
Si les fondations étaient fausses, l’un de ces contre-exemples pourrait aussi réfuter un théorème de base ; construire sur des fondations erronées a donc plutôt de fortes chances de révéler leurs défauts.
De même, lorsque les mathématiques sont parfois appliquées pour produire des prédictions, si les mathématiques sont fausses, les prédictions le seront aussi, et ces prédictions erronées attirent beaucoup l’attention.
En réalité, le mot « domaine » est un peu trompeur : beaucoup de théories ressemblent davantage à des nœuds liés à diverses autres théories dans l’ensemble des mathématiques.
Ces théories sont à leur tour reliées à d’autres.
Ce serait une situation très étrange si seules les fondations s’effondraient logiquement, sans aucun effet sur les autres parties de ce nœud.
Un énorme bloc flottant de mathématiques, entièrement cohérent en interne mais avec une seule erreur, est difficile à imaginer dans le cas de la cohomologie évoqué ici.
À strictement parler, c’est plutôt une posture philosophique, mais j’ai envie de croire qu’une grande partie des mathématiques actuelles a, en un certain sens, été découverte naturellement.
Pour spoiler : le monde a tout de même continué à tourner.
Depuis environ un an, j’essaie par intermittence de formaliser dans Lean une partie d’un cours de premier cycle en analyse complexe
Il y a eu beaucoup à apprendre et c’était gratifiant, mais parfois aussi frustrant
Ce n’est que récemment que j’ai réussi à définir complètement la forme polaire comme une bijection de C* vers (-pi,pi] x R, parce que je m’étais obstiné à la définir « depuis zéro », alors même que les nombres complexes, les séries entières, exp et sin existent déjà dans mathlib
Une grande partie de la difficulté vient probablement du fait que je n’ai qu’une licence de maths, que je ne suis pas familier avec Lean/mathlib et que je n’ai personne pour me guider. Cela dit, la communauté Zulip a été très utile
Beaucoup de résultats de mathlib sont formulés de manière assez abstraite, ce qui rend difficile de comprendre comment ils se rattachent aux théorèmes standards de premier cycle, ou même si ces théorèmes existent dans mathlib
C’est légitime pour la communauté des mathématiques de recherche, mais pour moi cela a été un gros obstacle, et si Lean est davantage utilisé dans l’enseignement, cela pourrait poser des problèmes similaires. Avec le temps, toutefois, c’est le genre de chose qui peut se clarifier
À mon avis, l’automatisation des preuves n’est pas encore suffisante
Trop de choses sont plus difficiles à prouver qu’elles ne devraient l’être, et ce qui me frustre le plus, ce sont surtout les conversions de types
En mathématiques ordinaires, les réels sont un sous-ensemble des complexes, donc tout ce qui est vrai pour tous les complexes est automatiquement vrai pour tous les réels ; dans Lean, ce sont des types différents, et il faut passer de l’un à l’autre au moyen de fonctions injectives / d’opérations de conversion, ce qui brouille le cœur de la preuve
Cela devient particulièrement sale quand les conversions de types s’empilent, par exemple des naturels vers les réels, puis vers les complexes
Bien sûr, c’est peut-être un problème propre au sujet ; dans des domaines comme l’algèbre, où l’on manipule explicitement des applications, cela doit paraître beaucoup plus naturel
Il est vraiment facile d’y obtenir de l’aide sur l’usage de mathlib, sur ce qui existe et où le trouver
Les problèmes de conversions de types empilées se résolvent généralement avec la tactique
norm_castMême sans question précise, si vous mentionnez ça en passant ou si quelqu’un voit dans votre code un style de preuve inutilement compliqué, on peut vous suggérer des tactiques que vous ne connaissiez pas
Si vous avez seulement l’impression que la formalisation est trop difficile sans savoir quelle technique utiliser, vous pouvez prendre une preuve insatisfaisante que vous avez péniblement construite, l’isoler en exemple autonome, et demander aux gens de la raccourcir
Ce genre de question est en général bien accueilli, et tout le monde apprend beaucoup
Ce fil semble porter sur la manière de bien écrire les mathématiques
J’ai lu, écrit, enseigné, appliqué et publié des mathématiques pendant des décennies, et j’ai aussi un doctorat en mathématiques appliquées
Il est vrai qu’il y a un problème dans l’écriture mathématique, et certaines mathématiques sont écrites de façon épouvantable
Mais il existe aussi des textes mathématiques plutôt bien écrits
Au minimum, tous les symboles doivent être définis avant usage ; il est utile de donner une motivation avant de présenter les mathématiques ; et parfois une explication intuitive est précieuse
Lire attentivement des textes mathématiques bien écrits aide à apprendre l’écriture mathématique
On peut citer par exemple Finite-Dimensional Vector Spaces de Paul R. Halmos, Advanced Calculus de R. Creighton Buck, Mathematical Analysis de Tom M. Apostol, Real Analysis de H. L. Royden, Real and Complex Analysis de Walter Rudin, Probability de Leo Breiman, et Mathematical Foundations of the Calculus of Probability de Jacques Neveu
L’auteur a essayé de vérifier le dernier théorème de Fermat exactement tel qu’il est développé dans la littérature, et il a découvert au passage qu’un lemme qui soutenait tout un sous-domaine n’était pas vrai sous la forme où il était utilisé
S’il croit néanmoins que ce domaine peut globalement être sauvé, c’est parce qu’il fait confiance au fait que, s’il était réellement faux, quelqu’un aurait déjà trouvé un résultat négatif
Il fallait donc maintenant trouver un substitut approprié pour soutenir ce domaine
L’auteur écrit de façon assez amusante ; c’était une expérience étrange, car je n’en comprenais qu’environ la moitié mais c’était quand même facile à lire
J’ai découvert vitiated, un bon mot à utiliser quand une preuve est réfutée ou qu’on y trouve un défaut
Je l’aime bien parce qu’il suggère que la preuve est abîmée et qu’il faut une nouvelle preuve ou une réparation, tout en risquant moins de laisser croire que la conclusion a été démontrée fausse