Une petite communauté de mathématiciens utilise Lean pour construire une nouvelle base numérique. Ils espèrent que cela assurera l'avenir de leur domaine scientifique.
Chaque jour, des dizaines de mathématiciens partageant les mêmes idées se rencontrent dans le chat Zulip pour travailler sur ce qu'ils pensent façonner l'avenir de leur domaine scientifique.
Ils sont tous fans du programme Lean . C'est un outil de démonstration de théorème interactif qui, en principe, est capable d'aider les mathématiciens à rédiger des preuves. Cependant, pour cela, les mathématiciens doivent entrer manuellement des règles mathématiques dans la base du programme, apportant les connaissances collectées au cours de milliers d'années à une forme qu'un ordinateur peut comprendre.
Pour de nombreux participants au projet, ses avantages nécessitent peu ou pas d'explication.
«À un niveau fondamental, il est évident qu'une fois qu'un élément est numérisé, il peut être utilisé de nouvelles manières», a déclaré Kevin Buzzardde l'Imperial College de Londres. "Et nous allons numériser les mathématiques pour les améliorer."
La numérisation des mathématiques est un vieux rêve. Les avantages attendus de cette gamme vont du trivial - vérifier les devoirs des élèves avec des ordinateurs - à l'extraordinaire: utiliser l'intelligence artificielle pour faire de nouvelles découvertes mathématiques et trouver de nouvelles solutions à d'anciens problèmes. Les mathématiciens croient que les prouveurs automatiques de théorèmes seront également capables de revoir les articles soumis à des revues, de trouver des erreurs que les critiques humains manquent parfois et de s'engager dans le travail technique fastidieux consistant à remplir la preuve avec tous les détails nécessaires.
Mais d'abord, les mathématiciens qui se rencontrent dans un chat ont besoin d'équiper Lean de connaissances dans le cadre des mathématiques scolaires, et jusqu'à présent, cette tâche n'est qu'à moitié terminée. Dans un proche avenir, il est peu probable que Lean puisse résoudre des problèmes ouverts, mais les personnes travaillant sur la base sont presque sûres que dans quelques années, le programme apprendra au moins à comprendre les problèmes au niveau des examens au lycée.
Qui sait? Les mathématiciens participant au projet n'ont pas toujours une idée claire de ce à quoi les mathématiques numériques peuvent être utiles.
«Nous ne savons pas exactement où nous allons», a déclaré Sébastien Gösel de l'Université de Rennes.
Vous planifiez, Lean fonctionne
Au cours de l'été, un groupe d'utilisateurs expérimentés de Lean a organisé un séminaire en ligne « Lean for Curious Mathematicians ». Dans la première leçon, Scott Morrison de l'Université de Sydney a montré comment écrire une preuve à l'aide d'un programme.
Il a commencé par écrire la déclaration qu'il voulait prouver en termes Lean. En langage humain, cela signifiait «il y a un nombre infini de nombres premiers». Il existe plusieurs façons de prouver cette affirmation, mais Morrison voulait utiliser une version légèrement modifiée de la première preuve trouvée par Euclide à partir de 300 avant JC. Dans la preuve, tous les nombres premiers connus sont multipliés, puis, après avoir ajouté 1, un nouveau nombre premier est obtenu (soit le produit lui-même, soit l'un de ses diviseurs sera premier). Le choix de Morrison était basé sur l'une des règles de base pour l'utilisation de Lean: l'utilisateur doit trouver lui-même l'idée principale de la preuve.
"Vous êtes responsable de la première supposition", a déclaré Morrison dans une interview.
Après avoir saisi l'assertion et choisi une stratégie, Morrison a esquissé la structure de la preuve en quelques minutes. Il a identifié une séquence d'étapes intermédiaires, dont chacune était relativement facile à prouver. Bien que Lean ne puisse pas offrir une stratégie de preuve générale, il peut vous aider à exécuter de petites étapes concrètes. Décomposant la preuve en sous-tâches accessibles, Morrison était un peu comme un chef demandant aux chefs ordinaires de hacher des oignons ou de faire bouillir de l'eau. «C'est là que vous espérez que Lean prendra le relais et commencera à vous aider», a déclaré Morrison.
Lean accomplit des tâches intermédiaires à l'aide de processus automatisés appelés tactiques. Ce sont des sortes d'algorithmes courts conçus pour effectuer des tâches très spécifiques.
Travaillant avec des preuves, Morrison a lancé une tactique appelée recherche de bibliothèque. Elle a passé au peigne fin la base de données mathématiques du programme et a renvoyé plusieurs théorèmes qui, selon elle, pourraient combler les lacunes dans une section particulière de la preuve. Différentes tactiques effectuent différentes tâches mathématiques. L'un d'eux, linarith, peut prendre un ensemble d'inégalités pour, disons, deux nombres réels, et confirmer la vérité de la nouvelle inégalité, qui comprend le troisième nombre: si a est 2 et b est supérieur à a, alors 3a + 4b est supérieur à 12. L'autre fait la plupart des travailler avec des règles algébriques de base telles que l'associativité.
«Il y a deux ans chez Lean, l'associativité devait être appliquée manuellement», a déclaré Amelia Livingston, étudiante en mathématiques à l'Imperial College de Londres qui étudie le Lean avec Buzzard. - Et puis quelqu'un a écrit une tactique qui le fait pour vous. Je suis content à chaque fois que je l’utilise. "
En tout, il a fallu 20 minutes à Morrison pour terminer la preuve d'Euclide. Ici et là, il compléta lui-même les détails; parfois les tacticiens le faisaient pour lui. Après chaque étape, Lean a vérifié la cohérence de la preuve par rapport aux règles logiques intégrées écrites dans un langage formel appelé théorie des types dépendants .
«Cela ressemble à une application Sudoku. Si vous faites un faux mouvement, il émet un bip », a déclaré Buzzard. En conséquence, Lean a confirmé la faisabilité de la preuve de Morrison.
C'était un exercice très amusant - comme c'est généralement le cas lorsque la technologie fait quelque chose pour vous. Cependant, la preuve d'Euclid existe depuis plus de 2000 ans. Les questions des mathématiciens d'aujourd'hui sont si complexes que Lean ne peut même pas comprendre les questions, encore moins aider à y répondre.
«Il faudra probablement des décennies pour que cet outil aide à la recherche», a déclaré Heather Macbeth de l'Université Fordham, l'une des utilisateurs de Lean.
Donc, avant que les mathématiciens puissent travailler avec Lean sur des questions qui les intéressent vraiment, ils doivent ajouter plus de règles mathématiques au programme. Et ceci, en fait, est une tâche assez simple.
Anatomie d'un programme de construction de preuves: Lean aide les mathématiciens à prouver des théorèmes en vérifiant le travail et en automatisant certaines étapes de la preuve.
1) Le mathématicien décrit la structure de base de la preuve et écrit la séquence des étapes en Lean.
2) La bibliothèque mathlib de programmes mathématiques a un ensemble de tactiques qui exécutent les étapes de cette preuve. Les mathématiciens continuent d'ajouter de nouvelles données à mathlib. Des théorèmes éprouvés sont ajoutés à mathlib.
3) L'algorithme Kernel vérifie l'exactitude de la preuve en utilisant des règles simples.
* La pieuvre est en quelque sorte devenue la désignation des émotions joyeuses dans la communauté Lean.
«Pour que Lean puisse comprendre quelque chose, les gens doivent traduire les manuels de mathématiques sous une forme que le programme puisse comprendre», a déclaré Morrison.
Malheureusement, la simplicité d'un problème ne signifie pas qu'il est facile à résoudre - étant donné qu'une grande partie des mathématiques ne sont pas couvertes dans les manuels.
Des connaissances éparses
Si vous n'avez pas étudié les mathématiques avancées, ce domaine peut vous sembler précis et bien décrit. Algèbre, calcul différentiel, analyse mathématique - tout découle de tout, et il y a des réponses à toutes les questions, énumérées à la fin du manuel.
Cependant, les mathématiques dans le programme scolaire, le programme d'études collégiales et même la majeure partie de l'université ne représentent qu'une petite partie de toutes les connaissances. La plupart d'entre eux ne sont pas bien organisés.
Il existe de vastes et importants domaines des mathématiques qui ne sont pas entièrement décrits. Ils sont stockés dans la tête d'un petit nombre de personnes qui ont appris leur sous-domaine des mathématiques des gens, l'ont appris de ceux qui les ont inventés - c'est-à-dire qu'ils existent sur la base du folklore.
Il y a d'autres domaines où le matériel de base a été écrit, mais il est si complexe et si long que personne n'a encore pu vérifier son exactitude. Au lieu de cela, les mathématiciens croient simplement en lui.
«Nous comptons sur la réputation de l'auteur. Nous savons qu'il est un génie et un homme méticuleux, donc la preuve est très probablement vraie », a déclaré Patrick Massot de l'Université Paris-Saclay.
C'est l'une des raisons pour lesquelles les programmes de démonstration de théorèmes sont si attrayants. Traduire les mathématiques dans un langage compréhensible par un ordinateur oblige les mathématiciens à enfin cataloguer leurs connaissances et à définir précisément tous les objets.
Assia Mabubide l'Institut d'État français pour la recherche en informatique et en automatisation se souvient de la première fois qu'elle a réalisé le potentiel d'une bibliothèque numérique aussi ordonnée: «J'étais fascinée par la possibilité de couvrir théoriquement toute la littérature mathématique en utilisant le langage de la logique pure, en stockant toute la bibliothèque mathématique sur un ordinateur, en vérifiant et en recherchant des données avec l'aide de programmes ".
Lean n'est pas le premier programme à avoir ce potentiel. Le premier, Automath, est apparu dans les années 1960, et Coq, l'un des plus populaires aujourd'hui, est sorti en 1989. Les utilisateurs de Coq ont formalisé beaucoup de mathématiques en langage de programme, mais ce travail était décentralisé et mal organisé. Les mathématiciens ne travaillaient que sur des projets qui les intéressaient et n'identifiaient que les objets dont ils avaient besoin pour leur propre travail, les décrivant souvent de manière unique. En conséquence, les bibliothèques pour Coq semblent encombrées, comme un plan pour une ville qui s'est développée naturellement.
«Coq est un vieil homme avec des cicatrices aujourd'hui», a déclaré Mabubi, qui a participé activement au programme. "Il a été soutenu par de nombreuses personnes pendant longtemps, et grâce à sa longue histoire, ses lacunes sont désormais bien connues."
En 2013, Leonardo de Mura , chercheur chez Microsoft, a lancé le projet Lean. Son nom [lean] reflète la volonté de de Moore de créer un programme efficace et propre. Il a supposé que le programme serait un outil pour vérifier l'exactitude du code d'autres programmes, et non des mathématiques. Cependant, il s'avère que vérifier l'exactitude d'un programme est un peu comme vérifier une preuve.
«Nous avons créé Lean parce que nous nous intéressons au développement de logiciels, et il existe une analogie entre la création de mathématiques et l'écriture de code», a déclaré de Moore.
Heather Macbeth de l'Université Fordham, l'une des utilisatrices de Lean
Au moment de la sortie de Lean, il y avait pas mal d'autres programmes d'aide, y compris Coq, qui est le plus similaire à Lean. La base logique des deux programmes est basée sur la théorie des types dépendants. Cependant, Lean offre une chance de recommencer.
Elle a rapidement attiré les mathématiciens. Ils l'ont utilisé avec un tel enthousiasme qu'ils ont commencé à prendre tout le temps libre de de Moore avec leurs questions sur le développement dans le domaine des mathématiques. "Il en a eu un peu marre des mathématiciens de premier plan et a dit - pourquoi ne créez-vous pas un référentiel séparé?" Dit Morrison.
Les mathématiciens ont créé cette bibliothèque en 2017. Ils l'appelèrent mathlib et se mirent avec zèle à le remplir de connaissances mathématiques mondiales, créant quelque chose comme un analogue de la Bibliothèque d'Alexandrie.au XXIe siècle. Les mathématiciens ont créé et téléchargé des extraits de mathématiques numérisées, créant progressivement un catalogue pour Lean. Et comme mathlib était nouveau, ils pouvaient apprendre des limites des systèmes antérieurs comme Coq et suivre la façon dont le matériel était organisé.
«Il y a une tentative délibérée de créer une bibliothèque mathématique monolithique, dont tous les fragments fonctionneront les uns avec les autres», a déclaré Macbeth.
Mathlib alexandrin
La page d'accueil du projet mathlib contient des graphiques montrant l'avancement du projet en temps réel. Le projet a une liste des leaders qui y investissent le plus, triés par le nombre de lignes de code [en premier lieu, soit dit en passant, est le mathématicien russe Yuri Kudryashov / env. trad.]. Le nombre total d'objets mathématiques numérisés est également calculé: début octobre, il contient 18 756 définitions et 39 157 théorèmes.
Tous ces ingrédients mathématiques peuvent être mélangés pour créer des mathématiques au sein de Lean. Jusqu'à présent, leur assortiment est très limité, malgré les chiffres apparemment impressionnants. Il n'y a presque rien des domaines de l'analyse complexe ou des équations différentielles - et ce sont deux éléments de base de nombreux domaines des mathématiques supérieures. De plus, le programme n'en sait pas encore assez pour décrire les problèmes du millénaire - des problèmes mathématiques définis par le Clay Mathematical Institute en 2000 comme «des problèmes classiques importants qui n'ont pas été résolus depuis de nombreuses années».
mathlib se remplit lentement mais sûrement. Le travail se déroule dans un esprit de travail d'équipe. Dans le chat Zulip, les mathématiciens sélectionnent les définitions qui nécessitent une formalisation, sont appelés à les écrire et fournissent des commentaires rapides sur le travail des autres.
«N'importe quel mathématicien de recherche peut étudier le mathlib et faire une liste de 40 choses qui ne sont pas là», a déclaré Macbeth. - Par conséquent, il décide de combler l'une de ces lacunes. Et le plaisir instantané est garanti - quelqu'un lira votre travail et laissera un commentaire à son sujet dans les 24 heures. "
De nombreux add-ons sortent petits - comme l'a découvert Sophie Morelde l'Ecole Normale de Lyon lors du séminaire en ligne "Lean for Curious Mathematicians". Les organisateurs de la conférence ont donné aux participants des énoncés mathématiques relativement simples à prouver dans la pratique Lean. En travaillant avec l'un d'eux, Morel s'est rendu compte que sa preuve nécessitait un lemme - un petit résultat intermédiaire - qui n'a pas été trouvé dans mathlib.
«C'était un petit morceau d'algèbre linéaire, qui, pour une raison quelconque, n'était pas encore là. Les personnes qui remplissent le mathlib essaient de tout saisir, mais vous ne pouvez pas prévoir toutes les options », a déclaré Morel, qui a elle-même entré le lemme requis en trois lignes dans la base.
D'autres contributions sont plus importantes. Depuis un an, Gösel travaille à la définition d'un collecteur lisse pour le mathlib. Les variétés lisses sont des ensembles (tels que des lignes, des cercles ou des surfaces d'une balle) qui jouent un rôle fondamental dans l'étude de la géométrie et de la topologie. Ils jouent aussi souvent un rôle important dans les problèmes de domaines tels que la théorie des nombres et le calcul. La plupart des recherches mathématiques sont impossibles sans eux.
Cependant, les variétés lisses peuvent se cacher sous différentes formes - tout dépend du contexte. Ils peuvent avoir un nombre fini ou infini de dimensions, avoir des limites ou ne pas en avoir, être définis sur divers systèmes de nombres - sur l'ensemble des réels, complexes ou p-adiquesNombres. Définir la diversité douce, c'est comme définir l'amour: vous le reconnaissez lorsque vous le rencontrez, mais toute définition stricte laissera sûrement tomber certains des exemples les plus évidents de ce phénomène.
«Lors de la définition des choses de base, vous n'avez pas à faire de choix», a déclaré Gösel. "Mais des objets plus complexes peuvent être formalisés de 10 à 20 manières différentes."
Gösel doit maintenir un équilibre entre spécificité et généralisation. «J'avais une règle - je voulais être en mesure de définir 15 utilisations différentes des variétés», dit-il. "En même temps, je ne voulais pas que la définition soit trop générale, sinon il serait impossible de travailler avec."
La définition qu'il a développée s'inscrit dans 1600 lignes de code - beaucoup pour une définition de mathlib, mais peut-être pas autant par rapport à toutes les possibilités mathématiques qu'il ouvre à Lean.
«Maintenant que nous avons le langage dont nous avons besoin, nous pouvons commencer à prouver des théorèmes», dit-il.
Trouver la définition correcte d'un objet du degré correct de généralité est la principale occupation des mathématiciens qui remplissent mathlib. Les créateurs de la bibliothèque espèrent définir les objets d'une manière qui est utile aujourd'hui, et en même temps suffisamment flexible pour que ces objets puissent être utilisés d'une manière imprévisible aujourd'hui.
«La nécessité que tout soit utile pour une utilisation dans un avenir lointain est soulignée», a déclaré Macbeth.
Les perfectoïdes sont nés de la pratique
Mais Lean n'est pas seulement un outil utile - il donne aux mathématiciens une chance de reprendre leur travail. Macbeth se souvient encore de la première fois qu'elle a essayé un programme pour aider à écrire des preuves. C'était en 2019 et le programme était Coq (bien qu'il soit maintenant passé à Lean). Elle ne pouvait pas s'arrêter.
«Lors d'un week-end fou, j'ai travaillé avec ce programme pendant 12 heures d'affilée», a-t-elle déclaré. "C'était une vraie addiction."
D'autres mathématiciens décrivent leurs expériences de la même manière. Lean, disent-ils, est comme un jeu d'ordinateur - jusqu'aux mêmes hormones de récompense qui rendent difficile la mise de côté d'un contrôleur de jeu. «Vous pouvez faire cela pendant 14 heures par jour sans vous sentir fatigué et dans un état élevé toute la journée», a déclaré Livingston. "Vous recevez des commentaires positifs tout le temps."
Sébastien Gösel
Pourtant, la communauté Lean comprend que pour de nombreux mathématiciens, il n'y a tout simplement pas assez de niveaux dans leur programme.
"Si vous quantifiez le pourcentage de mathématiques formalisées, je dirais que moins d'un millième de pour cent est encore prêt", a déclaré Christian Szegedi, un programmeur de Google travaillant sur des systèmes d'IA dont il rêve de pouvoir lire et formaliser de manière indépendante des manuels de mathématiques.
Mais les mathématiciens augmentent ce pourcentage. Si aujourd'hui mathlib contient la plupart du matériel enseigné par les étudiants de deuxième année, les participants au projet espèrent ajouter le reste du programme dans quelques années - et ce sera une réalisation importante.
«Au cours des 50 années de ces systèmes, personne n'a suggéré: asseyons-nous et organisons une base de connaissances cohérente en mathématiques, décrivant le matériel de l'institut», a déclaré Buzzard. "Nous créons une chose qui peut comprendre les questions de l'examen d'institut - cela ne s'est jamais produit auparavant."
Il faudra probablement des décennies avant que le contenu de mathlib corresponde à la bibliothèque de recherche, mais les utilisateurs Lean démontrent au moins la possibilité théorique de créer un tel catalogue - et atteindre cet objectif dépend simplement de la saisie de toutes les mathématiques dans la base de données sous forme de code de programme.
À cette fin, l'année dernière, Buzzard, Masso et Johan Kommelin de l'Université de Fribourg en Allemagne ont mis en œuvre un projet qui prouve la viabilité de ce rêve. Ils ont temporairement reporté le remplissage progressif de la base avec du matériel d'institut et sont passés à des zones avancées. Leur objectif était d'identifier l'une des plus grandes innovations en mathématiques du 21e siècle - un objet tel que «l'espace perfectoïde» développé au cours des dix dernières années par Peter Scholze de l'Université de Bonn. En 2018, il a reçu le prix Fields pour son travail, le plus grand prix en mathématiques.
Buzzard, Masso et Commelin voulaient démontrer que, du moins en principe, Lean peut travailler avec des mathématiques qui intéressent vraiment les mathématiciens. "Ils ont pris quelque chose de très complexe et nouveau et ont montré que ces objets peuvent être manipulés avec un programme pour aider à écrire des preuves", a déclaré Mabubi.
Kevin Buzzard
Pour définir un espace perfectoïde, trois mathématiciens devaient combiner plus de 3 000 définitions d'objets mathématiques et 30 000 connexions entre eux. Les définitions se sont étendues à de nombreux domaines des mathématiques, de l'algèbre à la topologie et à la géométrie. Les rassembler en une seule définition était une démonstration puissante de la croissance de la complexité des mathématiques au fil du temps - et pourquoi il est si important de jeter les bases de mathlib.
«De nombreux domaines des mathématiques avancées exigent que vous connaissiez toutes sortes de mathématiques enseignées aux élèves», a déclaré Macbeth.
La Trinité a réussi à définir l'espace perfectoïde, mais jusqu'à présent, les mathématiciens ne peuvent pas faire grand-chose. Beaucoup plus de définitions mathématiques sont nécessaires en Lean, jusqu'à ce que le programme puisse au moins formuler les questions difficiles dans lesquelles ces espaces perfectoïdes surgissent.
"C'est assez idiot que Lean sache ce qu'est un espace perfectoïde, mais ne connaît pas une analyse complexe", a déclaré Masso.
Buzzard est d'accord avec lui, qualifiant la formalisation de l'espace perfectoïde de "gadget" - une astuce qui montre parfois que les nouvelles technologies démontrent leur utilité. Et cette fois, l'astuce a fonctionné.
"Vous n'êtes pas obligé de penser que grâce à notre travail, tous les mathématiciens de la Terre ont commencé à utiliser des programmes pour aider à écrire des preuves", a déclaré Masso, "mais je pense que beaucoup d'entre eux ont remarqué cette possibilité et ont commencé à poser des questions."
Il faudra beaucoup de temps avant que le Lean ne devienne une véritable partie de la recherche mathématique. Cependant, cela ne signifie pas qu'aujourd'hui le programme est une image de la science-fiction. Les mathématiciens impliqués dans son développement comparent leur travail à la pose des premières voies ferrées - le démarrage nécessaire d'une entreprise importante, même s'ils ne peuvent pas eux-mêmes emprunter la voie.
«Ce sera une chose tellement cool que cela en vaut la peine aujourd'hui», a déclaré Macbeth. «J'investis mon temps en elle aujourd'hui afin que quelqu'un dans le futur puisse vivre une expérience aussi incroyable en travaillant avec elle.