Peter Scholze veut reconstruire une grande partie des mathématiques modernes, en partant de l'une de ses pierres angulaires. Maintenant, il a reçu la validation d'une preuve au cœur de sa quête d'une source improbable : un ordinateur.
Bien que la plupart des mathématiciens doutent que les machines remplacent de sitôt les aspects créatifs de leur profession, certains reconnaissent que la technologie jouera un rôle de plus en plus important dans leurs recherches, et cet exploit particulier pourrait être un tournant vers son acceptation.
Scholze, un théoricien des nombres, a présenté le plan ambitieux - qu'il a co-créé avec son collaborateur Dustin Clausen de l'Université de Copenhague - dans une série de conférences en 2019 à l'Université de Bonn, en Allemagne, où il est basé . Les deux chercheurs l'ont surnommé "mathématiques condensées", et ils disent qu'il promet d'apporter de nouvelles connaissances et de nouveaux liens entre des domaines allant de la géométrie à la théorie des nombres.
D'autres chercheurs sont attentifs : Scholze est considéré comme l'une des étoiles les plus brillantes des mathématiques et a fait ses preuves dans l'introduction de concepts révolutionnaires. Emily Riehl, mathématicienne à l'Université Johns Hopkins de Baltimore, dans le Maryland, affirme que si la vision de Scholze et Clausen se concrétise, la façon dont les mathématiques seront enseignées aux étudiants diplômés dans 50 ans pourrait être très différente de ce qu'elle est aujourd'hui. "Il y a beaucoup de domaines des mathématiques qui, je pense, seront affectés par ses idées à l'avenir", dit-elle.
Jusqu'à présent, une grande partie de cette vision reposait sur une preuve technique si complexe que même Scholze et Clausen ne pouvaient pas être sûrs qu'elle était correcte. Mais plus tôt ce mois-ci, Scholze a annoncé qu'un projet visant à vérifier le cœur de la preuve à l'aide d'un logiciel informatique spécialisé avait été couronné de succès.
Assistance informatique
Les mathématiciens utilisent depuis longtemps les ordinateurs pour effectuer des calculs numériques ou manipuler des formules complexes. Dans certains cas, ils ont prouvé des résultats majeurs en obligeant les ordinateurs à effectuer d'énormes quantités de travail répétitif - le plus célèbre étant une preuve dans les années 1970 que n'importe quelle carte peut être colorée avec seulement quatre couleurs différentes, et sans remplir deux pays adjacents avec le même couleur.
Le prodige de la théorie des nombres parmi les lauréats du prix le plus convoité en mathématiques
Mais les systèmes connus sous le nom d'assistants de preuve vont plus loin. L'utilisateur entre des instructions dans le système pour lui apprendre la définition d'un concept mathématique - un objet - basé sur des objets plus simples que la machine connaît déjà. Une déclaration peut également se référer uniquement à des objets connus, et l'assistant de preuve répondra si le fait est "évidemment" vrai ou faux sur la base de ses connaissances actuelles. Si la réponse n'est pas évidente, l'utilisateur doit entrer plus de détails. Les assistants de preuve forcent ainsi l'utilisateur à exposer la logique de leurs arguments de manière rigoureuse, et ils remplissent des étapes plus simples que les mathématiciens humains avaient consciemment ou inconsciemment sautées.
Une fois que les chercheurs ont accompli le travail acharné de traduction d'un ensemble de concepts mathématiques en un assistant de preuve, le programme génère une bibliothèque de code informatique qui peut être exploitée par d'autres chercheurs et utilisée pour définir des objets mathématiques de niveau supérieur. De cette manière, les assistants de preuve peuvent aider à vérifier des preuves mathématiques qui seraient autrement longues et difficiles, voire pratiquement impossibles, à vérifier pour un humain.
' théorie de la grande unification " title="Les mathématiciens accueillent favorablement la preuve assistée par ordinateur dans la théorie de la "grande unification"" >
Les assistants de preuve ont depuis longtemps leurs fans, mais c'est la première fois qu'ils jouent un rôle majeur à la pointe d'un domaine, déclare Kevin Buzzard, mathématicien à l'Imperial College de Londres qui faisait partie d'une collaboration qui a vérifié Résultat de Scholze et Clausen. « La grande question qui restait était : peuvent-ils gérer des mathématiques complexes ? » dit Buse. "Nous avons montré qu'ils le pouvaient."
Et tout s'est passé beaucoup plus vite que quiconque ne l'avait imaginé. Scholze a présenté son défi aux experts en assistants de preuve en décembre 2020, et il a été relevé par un groupe de volontaires dirigé par Johan Commelin, mathématicien à l'Université de Fribourg en Allemagne. Le 5 juin - moins de six mois plus tard - Scholze a publié sur le blog de Buzzard que la majeure partie de l'expérience avait réussi. "Je trouve absolument insensé que les assistants de preuve interactifs soient maintenant au niveau où, dans un laps de temps très raisonnable, ils peuvent formellement vérifier des recherches originales difficiles", a écrit Scholze.
Le génie des mathématiques de l'IA crée de nouveaux problèmes difficiles à résoudre pour les humains
Le point crucial des mathématiques condensées, selon Scholze et Clausen, est de redéfinir le concept de topologie, l'une des pierres angulaires des mathématiques modernes. Beaucoup d'objets étudiés par les mathématiciens ont une topologie - un type de structure qui détermine quelles parties de l'objet sont proches les unes des autres et lesquelles ne le sont pas. La topologie donne une idée de la forme, mais plus malléable que celles de la géométrie familière de niveau scolaire : en topologie, toute transformation qui ne déchire pas un objet est admissible. Par exemple, tout triangle est topologiquement équivalent à tout autre triangle - ou même à un cercle - mais pas à une ligne droite.
La topologie joue un rôle crucial non seulement en géométrie, mais aussi dans l'analyse fonctionnelle, l'étude des fonctions. Les fonctions « vivent » généralement dans des espaces avec un nombre infini de dimensions (comme les fonctions d'onde, qui sont à la base de la mécanique quantique). C'est également important pour les systèmes de nombres appelés nombres p-adiques, qui ont une topologie « fractale » exotique.
Une grande unification
Vers 2018, Scholze et Clausen ont commencé à se rendre compte que l'approche conventionnelle du concept de topologie entraînait des incompatibilités entre ces trois univers mathématiques - la géométrie, l'analyse fonctionnelle et les nombres p-adiques - mais que des fondations alternatives pourraient combler ces lacunes. De nombreux résultats dans chacun de ces domaines semblent avoir des analogues dans les autres, même s'ils traitent apparemment de concepts complètement différents. Mais une fois que la topologie est définie de manière "correcte", les analogies entre les théories se révèlent être des instances des mêmes "mathématiques condensées", ont proposé les deux chercheurs. "C'est une sorte de grande unification" des trois domaines, dit Clausen.
Scholze et Clausen disent qu'ils ont déjà trouvé des preuves plus simples et "condensées" d'un certain nombre de faits géométriques profonds, et qu'ils peuvent maintenant prouver des théorèmes qui étaient auparavant inconnus. Ils ne les ont pas encore rendus publics.
Il y avait cependant un hic : pour montrer que la géométrie s'inscrivait dans cette image, Scholze et Clausen ont dû prouver un théorème hautement technique sur l'ensemble des nombres réels ordinaires, qui a la topologie d'une ligne droite. "C'est comme le théorème fondamental qui permet aux nombres réels d'entrer dans ce nouveau cadre", explique Commelin.
Clausen rappelle comment Scholze a travaillé sans relâche sur la preuve jusqu'à ce qu'elle soit achevée "par la force de la volonté", produisant de nombreuses idées originales dans le processus. "C'était l'exploit mathématique le plus incroyable que j'aie jamais vu", se souvient Clausen. Mais l'argument était si complexe que Scholze lui-même craignait qu'il puisse y avoir une lacune subtile qui invaliderait toute l'entreprise. "Cela avait l'air convaincant, mais c'était tout simplement trop nouveau", déclare Clausen.
Pour obtenir de l'aide pour vérifier ce travail, Scholze s'est tourné vers Buzzard, un collègue théoricien des nombres qui est un expert en Lean, un progiciel d'assistant de preuve. Lean a été créé à l'origine par un informaticien de Microsoft Research à Redmond, Washington, dans le but de vérifier rigoureusement le code informatique à la recherche de bogues.
Buzzard avait mis en place un programme pluriannuel pour encoder l'intégralité du programme de mathématiques de premier cycle de l'Impérial en Lean. Il avait également expérimenté l'entrée de mathématiques plus avancées dans le système, y compris le concept d'espaces perfectoïdes, qui a aidé à gagner la médaille Scholze a Fields en 2018.
Commelin, qui est également un théoricien des nombres, a pris l'initiative de vérifier la preuve de Scholze et Clausen. Commelin et Scholze ont décidé d'appeler leur projet Lean Liquid Tensor Experiment, en hommage au groupe de rock progressif Liquid Tension Experiment, dont les deux mathématiciens sont fans.
Une collaboration en ligne fébrile s'ensuit. Une douzaine de mathématiciens ayant une expérience du Lean se sont joints à nous, et les chercheurs ont été aidés par des informaticiens en cours de route. Début juin, l'équipe avait entièrement traduit le cœur de la preuve de Scholze - la partie qui l'inquiétait le plus - en Lean. Et tout a été vérifié — le logiciel a pu vérifier cette partie de la preuve.
Meilleure compréhension
La version allégée de la preuve de Scholze comprend des dizaines de milliers de lignes de code, 100 fois plus longues que la version originale, déclare Commelin. "Si vous regardez simplement le code Lean, vous aurez beaucoup de mal à comprendre la preuve, surtout telle qu'elle est maintenant." Mais les chercheurs disent que l'effort de faire fonctionner la preuve dans l'ordinateur les a également aidés à mieux la comprendre.
LINK AI Copernicus "découvre" que la Terre tourne autour du Soleil
Riehl fait partie des mathématiciens qui ont expérimenté les assistants de preuve, et les enseigne même dans certains de ses cours de premier cycle. Elle dit que, bien qu'elle ne les utilise pas systématiquement dans ses recherches, elles ont commencé à changer sa façon même de penser les pratiques de construction de concepts mathématiques et d'énoncer et de prouver des théorèmes à leur sujet. "Auparavant, je pensais prouver et construire à partir de deux choses différentes, et maintenant je les considère comme identiques."
De nombreux chercheurs affirment qu'il est peu probable que les mathématiciens soient remplacés par des machines de sitôt. Les assistants de preuve ne peuvent pas lire un manuel de mathématiques, ils ont besoin d'une contribution continue des humains et ils ne peuvent pas décider si un énoncé mathématique est intéressant ou profond - seulement s'il est correct, dit Buzzard. Pourtant, les ordinateurs pourraient bientôt être en mesure de signaler les conséquences des faits connus que les mathématiciens n'avaient pas remarqués, ajoute-t-il.
Scholze dit qu'il a été surpris de voir jusqu'où les assistants de preuve pouvaient aller, mais qu'il n'est pas sûr qu'ils continueront à jouer un rôle majeur dans ses recherches. "Pour l'instant, je ne vois pas vraiment comment ils pourraient m'aider dans mon travail de création en tant que mathématicien."
