Logiciel lean
Bonsoir,
certains d'entre vous travaillent-ils sur des systèmes formels dernière génération comme "Lean" ?
Lean (de Microsoft Research) est à la fois un langage de programmation et un assistant de preuves. Il utilise un formalisme logique très $\textbf{expressif}$ puisqu'il permet de formaliser plus directement des énoncés particulièrement riches issus de domaines comme la topologie différentielle, l'analyse complexe ou la géométrie algébrique.
Du moins c'est ce que j'en ai compris.
À tel point que des équipes, de par le monde, se sont données pour défi de lui "enseigner" la théorie des schémas affines de Grothendieck, celle des espaces perfectoïdes de Scholze ou encore la théorie abstraire de l'homotopie. Les mathématiciens qui cherchent à traduire leurs énoncés dans le cadre de ces nouveaux langages font face à de gros problèmes techniques résolus tant bien que mal par des informaticiens qui n'ont, pour la plupart, jamais entendus parler de ces théories.
Les échanges entre informatique théorique et mathématiques se révèlent pourtant fructueux. Ainsi, certaines avancées mathématiques peuvent se "lire" comme des résultats formels en théorie des types. Les chercheurs espèrent découvrir un jour les nouveaux théorèmes de leur discipline dans le langage proposé par le système lui-même. Grâce au "deep learning", plus il "travaille", moins il a recourt aux masses de données fournies par les humains. Je trouve cela franchement hallucinant !
Ci-dessous : quelques lignes de code parmi plusieurs dizaines de milliers destinées à apprendre les principes et définitions de base de la théorie perfectoïde à un ordinateur.
Un grand nombre de ces lignes sont consacrées, par exemple, aux anneaux topologiques. Certaines ont été élaborées par des équipes de Paris-Sud (Patrick Massot) et toutes finiront par intégrer la "librairie" du système. Le but étant de savoir si ce-dernier est en mesure de manipuler des objets d'une telle complexité.
Il semble que ce soit le cas puisque LEAN qui, il y a 18 mois de cela, ne savait même pas ce qu'était un nombre complexe, commence à vérifier par lui-même la validité de certaines définitions.
La production de résultats intéressants dans le cadre de théories mathématiques très avancées n'est cependant pas pour demain car il reste à comprendre ce que le système comprend exactement de tout ce qu'il ingurgite ! Cela passe par une meilleure maîtrise des langages formels : une formation bientôt indispensable pour le mathématicien du futur.
En lien : "Schemes in Lean". L'auteur du blog "XENA Project" évoque ses travaux sur les systèmes formels.
...
certains d'entre vous travaillent-ils sur des systèmes formels dernière génération comme "Lean" ?
Lean (de Microsoft Research) est à la fois un langage de programmation et un assistant de preuves. Il utilise un formalisme logique très $\textbf{expressif}$ puisqu'il permet de formaliser plus directement des énoncés particulièrement riches issus de domaines comme la topologie différentielle, l'analyse complexe ou la géométrie algébrique.
Du moins c'est ce que j'en ai compris.
À tel point que des équipes, de par le monde, se sont données pour défi de lui "enseigner" la théorie des schémas affines de Grothendieck, celle des espaces perfectoïdes de Scholze ou encore la théorie abstraire de l'homotopie. Les mathématiciens qui cherchent à traduire leurs énoncés dans le cadre de ces nouveaux langages font face à de gros problèmes techniques résolus tant bien que mal par des informaticiens qui n'ont, pour la plupart, jamais entendus parler de ces théories.
Les échanges entre informatique théorique et mathématiques se révèlent pourtant fructueux. Ainsi, certaines avancées mathématiques peuvent se "lire" comme des résultats formels en théorie des types. Les chercheurs espèrent découvrir un jour les nouveaux théorèmes de leur discipline dans le langage proposé par le système lui-même. Grâce au "deep learning", plus il "travaille", moins il a recourt aux masses de données fournies par les humains. Je trouve cela franchement hallucinant !
Ci-dessous : quelques lignes de code parmi plusieurs dizaines de milliers destinées à apprendre les principes et définitions de base de la théorie perfectoïde à un ordinateur.
Un grand nombre de ces lignes sont consacrées, par exemple, aux anneaux topologiques. Certaines ont été élaborées par des équipes de Paris-Sud (Patrick Massot) et toutes finiront par intégrer la "librairie" du système. Le but étant de savoir si ce-dernier est en mesure de manipuler des objets d'une telle complexité.
Il semble que ce soit le cas puisque LEAN qui, il y a 18 mois de cela, ne savait même pas ce qu'était un nombre complexe, commence à vérifier par lui-même la validité de certaines définitions.
La production de résultats intéressants dans le cadre de théories mathématiques très avancées n'est cependant pas pour demain car il reste à comprendre ce que le système comprend exactement de tout ce qu'il ingurgite ! Cela passe par une meilleure maîtrise des langages formels : une formation bientôt indispensable pour le mathématicien du futur.
En lien : "Schemes in Lean". L'auteur du blog "XENA Project" évoque ses travaux sur les systèmes formels.
...
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
-- Schnoebelen, Philippe
Pour ce qui est d'une entreprise américaine, n'étant pas expert en droit commercial: je n'en sais rien.
Tu trouveras certainement en cliquant ici: https://github.com/leanprover/theorem_proving_in_lean/blob/master/LICENSE
...
Enfin j'espère !
Si je suis suivi dans la rue par des limousines noires aux vitres teintées, je commencerai à m'en inquiéter.
...
1/ j'invite à googler le mot "lean" (y compris sa traduction en français), c'est très édifiant.
2/ Je trouve dommage l'usage de mots snobs et trompeurs souvent observé dans ce type de communication depuis quelques années (je ne crois pas qu'on puisse parler de décennies): homotopie, géométrie algébrique, etc. On en avait parlé il y a un an. La ré-invention de l'eau chaude par des non-logiciens (la correspondance de Curry Howard), COQ, etc qui se retrouve présentée de manière "ésotérique" avec des grands mots, pour tenter de la "distinguer" de l'avant ne me parait pas de bon gout, pour le dire gentiment, et même très inquiétante.
On est en science, quand des scientifiques s'improvisent communiquants, il y a de quoi s'inquiéter. Les cataliseurs-prouveurs logiciels marchent tous sur le même principe (4 lignes de code + des interface de convivialité). Laisser croire au grand public qu'il en irait autrement n'est pas sympathique.
L'introduction éventuelle (ça n'apparait pas encore dans les quelques pages internet sur lean (rares)) de "perceptronisme" ** posera une vraie question si elle survient, d'autant qu'il faudra mettre une paroi très solide et étanche entre l'aide à l'inspiration et la vérification de preuves.
[small]** c'est la partie scientifique qui "éduque" les réseaux de neurones, avec, c'est à signaler une IGNORANCE par essence des modifications internes de la machine une fois qu'elle a été éduquée (par éduquer on entend un petit algorithme qui modifie des paramètres en temps réel au fur et à mesure qu'on lui signale qu'elle s'est trompée de façon à obtenir des interpolations de plus en plus efficaces. Ca existe depuis quasiment un siècle, c'est ainsi que sont réglés les lecteurs de code barre, etc.[/small]
Je vous conseille la lecture de The future of mathematics ? de Kevin Buzzad.
Je me demande combien il a touché pour dire ça.
J'ajouterais que de nombreux contributeurs au projet sont extérieur à ce labo.
-- Schnoebelen, Philippe
"7 types de structures doivent être explicitement déclarées avant de pouvoir formaliser un anneau topologique (topological ring)."
La lourdeur de certaines procédures risque de freiner l'intuition du chercheur. Déjà complexes quand il s'agit de décrire un semi-groupe, elles deviennent pratiquement ingérables quand on s'attaque aux "produits tensoriels de bi-modules" !
J'imagine que les concepteurs de ces systèmes vont tenir compte des critiques des mathématiciens.
...
"lean" et "Coq" partagent un même langage formel baptisé CIC ("Calculus of Inductive Constructions") et dont les règles d'inférence sont décrites dans ce lien: https://coq.inria.fr/refman/language/cic.html
Il peut également être retrouvé dans le lien posté par @Héhéhé.
"Coq" présente un point de vue " constructif " dans lequel tous les objets (ou termes) appartiennent à différents types.
Les types eux-mêmes appartiennent à des types. On appelle $"\textbf{sorts}"$ les types de types: je ne sais pas comment ça se traduit.
Il y a deux sortes de "sorts": les propositions ($\textbf{Prop}$) appartenant au type des propositions logiques et les "petits ensembles" ($\textbf{Set}$) regroupant diverses fonctions. À noter que dans CIC, les preuves elles-mêmes sont considérées comme des "termes".
CIC contient aussi des langages annexes dont un, le "langage des tactiques" ou $\textbf{Ltac}$ permet à l'utilisateur de construire sa preuve de manière interactive. Il prend en charge différentes "tactiques".
Je poste ce fichier: $\textbf{"Contributions to the formal verification of arithmetic algorithms"}$ par $\textbf{Erik Martin-Dorel}$-ENS Lyon.
Je n'ai pu que le survoler car sa compréhension nécessite de toute évidence une solide formation de logicien. Il décrit le fonctionnement de "Coq" et sa logique constructive. L'étude des "tactiques" figure en page 50.
C'est la notion même de preuve qui est questionnée par ces nouveaux outils. L'objectif des systèmes actuels est de garantir la validité de toutes les preuves contenues dans une théorie mathématique donnée. Sauf que certains systèmes ne considèrent pas de simples vérifications comme des preuves alors que d'autres si. Ces nuances sont directement liées au type de logique privilégié par le système.
La philosophie de la preuve est décrite en introduction de la thèse de Dorel.
...
Ce qui fait que tous ces logiciels sont des usines à gaz vient d'une erreur de paradigme je l'ai dit 4837272747 fois sur ce forum.
Le bon paradigme consiste à EXTRAIRE les axiomes d'un raisonnement et non pas à BRIDER les raisonnements.
Led logiciels qui conviendront un jour sont ceux qui produiront la liste d'admis des entrées qu'on leur proposera.
Finalement, on procède avec les systèmes de preuve comme avec les humains: pas à pas, en commençant par les techniques de localisation dans les anneaux et les fondamentaux de l'algèbre commutative.
https://xenaproject.wordpress.com/
...
Par exemple, ces derniers mois, Lean a dû ingurgiter des chapitres entiers des EGA IV de Grothendieck. Ce qui est cruel, même pour une machine.
Les collègues de Kevin Buzzard ont proposé à leur système, l'exercice suivant (en théorie des catégories infinies) mais je n'ai pas bien compris si l'expérience avait été concluante.
Pour ce qui est de réaliser des démonstrations complexes, comme ce théorème de Deligne sur les représentations galoisiennes, on est encore très loin du compte quelque soit le système envisagé: ce qui est heureux pour les mathématiciens de chair et de sang ! J'ai lu un article sur "Nature": certains redoutent de devenir eux-mêmes des "assistants de preuve" ou à se voir déposséder de leur discipline.
...
...
Par ailleurs, je vois l'exercice donné, qui est un peu le truc le "plus basique" auquel on peut penser une fois que la notion de quasi-catégorie a été définie. Aurais-tu un lien où il est question de la formalisation en Lean des $\infty$-catégories (voire juste des quasi-catégories)? Ça m'intéresse pas mal.
Et puisque tu as l'air de t'être un peu intéressé au sujet des assistants de preuves, j'ai cru entendre que, pour l'instant, Coq, avec sa librairie HoTT, était plus ou moins le "mieux" pour faire de la théorie des catégories avec un assistant de preuve. Est-ce vrai? Est-ce que Lean est proche de rattraper Coq/Hott sur ce sujet?
Edit: Je vois les magnifiques diagrammes que tu as postés, je ne vois pas où est-ce qu'il faudrait un "système de preuve":-D. Ces diagrammes commutatifs (ou plutôt, diagrammes plans, vu qu'il y a des $2$-cellules) obéissent déjà à des règles, et ils sont une manière d'encoder des calculs/équations de manière graphique, tout comme lorsqu'on écrit une équation avec des symboles. Si le passage d'un diagramme à un autre est justifié (par exemple, par la commutativité d'un sous-diagramme ou par des règles de compatibilité entre les différentes cellules), pas besoin de plus que ces diagrammes :-D. Il n'y pas plus besoin d'un système de preuve qu'il n'en faudrait un pour vérifier des gros calculs avec plein de termes qui prennent plusieurs lignes.
Bon, en vrai, je cracherais pas sur un bidule qui vérifierait automatiquement la commutativité de certains diagrammes :-P.
Edit 2: Je me rends compte que j'ai peut-être mal interprété ton message, et que tu voulais peut-être simplement dire que ces pauvres assistants de preuves allaient bouffer des bons gros diagrammes comme ça. La fatigue surement.
Lemme d'échange, plongement de Yoneda, adjonction, limites, catégories cartésiennes closes, théorème du foncteur adjoint de Freyd: tout cela te parle-t-il ? À moi: très peu ! Ces définitions ont été formalisées sur Coq. J'ignore si Lean est plus avancé mais j'attache une brève description de sa bibliothèque en théorie des catégories: elle est en constante évolution bien sûr.
Pour ce qui est de la théorie infinie: je ne sais où en sont les différents systèmes.
J'ai cru comprendre que Coq est très difficilement lisible et exploitable par des mathématiciens dits "purs" sans de solides connaissances en théorie des types.
...
C'est une nécessité car la théorie des espaces perfectoïdes de Peter Scholze (dont les définitions intègrent peu à peu le corpus de Lean) contient une partie liée aux catégories infinies. Je rajoute le pdf sur la théorie des catégories infinies d'où est tiré l'exercice 1.1.i (attention: c'est d'une violence inouïe !) ainsi qu'une interview d'un chercheur de l'ENS qui décrit son travail avec Coq.
ps: inutile de préciser que ça ou un texte en Mandarin, pour moi c'est égal !
...
Sinon, pour le second pdf, Riehl-Verity, c'est effectivement assez violent, ça ne m'étonne pas que ça te rebute! En plus, il me semble que ce livre est toujours en construction. Il y a des références plus accessibles sur le sujet, par exemple, le livre de Denis-Charles Cisinski, qu'il met gratuitement à disposition sur sa page: http://www.mathematik.uni-regensburg.de/cisinski/CatLR.pdf .
Je suis tombé sur ce fil y'a quelques semaines et j'ai essayé de faire tourner le joujou ! Bon c'est un peu galère au début d'y comprendre quelques choses mais j'ai réussi à encoder une petite preuve (mon premier théorème :-D) et finalement c'est pas trop complexe (après je ne sais pas combien d'heures de galère), du coup je vous fait l'exemple avec quelques explications :
cf l'image le code source ne passe pas !
La première ligne c'est les présentations et dire que $G$ sera un groupe ce qui permet l'utilisation de certaines règles de base sur les groupes (j'ai comme petit projet de tout programmer la structure de groupe histoire de mieux comprendre).
Ensuite la présentation du théorème : c'est très proche du niveau mathématique (ce qui est assez sympa) ! Les symboles que l'on voit c'est plus ou moins du code latex \forall \to etc
Ensuite l'environnement calc, toutes les lignes de calculs doivent être justifiées par une règle. La première ligne doit se lire par re-écriture de l'hypothèse $h$ appliquée à $a * b$ !
La seconde ligne est spéciale elle utilise une simplification automatique via simp (i.e on laisse la machine se débrouiller pour chercher quelle méthode utiliser pour justifier le calcul) ici la règle est rw mul_inv_rev (faut aller regarder dans le codage de "group") !
Voilà ma toute petite contribution ! Pour tout dire, j'ai essayé y'a quelques années de faire des choses avec coq et je ne suis arrivé à strictement rien du tout ici y'a peut-être moyen que ce soit un poil plus parlant pour les matheux $\lambda$ !
Faudrait demander à Foys de nous montrer comment on peut faire en Coq, s'il passe par ici !
Je vous transmets le message de quelqu'un qui travaille beaucoup sur le projet (ce n'est pas moi qui parle :-D).
Tout ce que tu mentionnes nécessite des centaines de démonstrations. Pour analogie élémentaire : " Est-ce que pour définir les nombres réels avec leur topologie et leur structure de corps » n'est " que définitions " ou bien il faut démontrer des choses ?
Cette histoire de maths constructives n'est pas du tout obligatoire quand on utilise un assistant de démonstrations.
Comme quoi, on peut quasiment tout apprendre en s'amusant, c'est super !
Pour ma part, je vais essayer !
J'ai l'impression qu'il y a aussi un tutoriel sur ça ici. La bibliothèque mathématique de lean, avec les choses déjà formalisées, est ici, il y a l'air d'y avoir déjà quelques choses de faites, mais qui restent somme toute assez basiques.
Ce qui est un peu dommage, c'est le manque d'une documentation centralisée, là, quand on cherche comment faire un truc, on ne tombe que sur des tutoriels qui montrent des exemples du truc en action, mais pas de belle doc qui donne exactement le fonctionnement de la chose. C'est sûrement du au fait que le truc est encore en construction surement, mais c'est un peu dommage!
En tout cas merci encore Héhéhé pour ce petit lien, j'ai maintenant vraiment très envie de rentrer un peu plus dans lean :-D
Viens sur le chat zulip si tu as des questions, j'essayes d'apprendre la gestion des catégories c'est hard hard !
PS. Je n'ai pas réussi à construire le site affine, l'axiome de transitivité est vraiment délicat je sens que ça va me prendre des années :-D
flipflop: quel éditeur utilises-tu qu'on voit sur ton screenshot ?
C'est vs code studio :
Lien ici faire attention a vraiment suivre le processus à la lettre sinon ça bug ! (par exemple sous windows faire attention au moment d'installer python, d'activer la variable d'environement).
Sinon un cours en français : ici orienté analyse L1. C'est plutôt pas mal pour nous autres matheux :-D
une petite vidéo : ici
Encore une fois n'hésitez pas a poser des questions sur le chat zulip que j'ai mis en lien en l'autre message, les gens sont cools avec les débutants. Mais dans tous les cas ça demande vraiment un effort pour prendre en main le truc !
Comment va ? La gestion des catégories sous lean, c'est pas un thème un peu trop facile que tu as choisi, non ?
De mon côté, je continue à faire comme d'habitude c'est-à-dire n'importe quoi.
Bien à toi.
C'est très amusant comme thème, je suis entrain de programmer tous mes petits jouer ! Par contre, c'est un peu délicat pour l'instant de définir la notion de foncteur local ! Je n'ai pas encore l'espace projectif et tout mais ca viendra après je vais faire des tours de magie $\otimes$ et je vais faire agir plein de groupe dans tous les sens et je vais peut être réussir a prouver que mon foncteur $\Gamma : \text{Ring} \to \text{Ens}$ donné par $$
R \mapsto \{(x,\iota) \in R \times R/xR \mid \iota^2+1 = \}
$$
est un bidule algébrique, après je vais étudier son fibré tangent et tout :-D
Ps / Tu vois moi aussi je fais n'importe quoi :-D
Le genre de questions que je me pose:
* quelles sont les différences entre (x : X), [x : X] et {x : X};
* quelle est la différence entre structure et class et pourquoi diable marche alors que ne marche pas ?
* Comment accéder à f dans mon exemple précédent si on travaille avec class?
* Si je déclare deux groupes (qui ont l'air d'être fait construit avec class) et que je fais le produit de deux éléments j'ai utilisé la loi de $G$ ou la loi de $H$ ?
* Comment montrer que $(\mathbb Z,+)$ est un magma ? J'ai l'impression qu'on peut utiliser instance mais je ne suis arrivé à rien.
Bref c'est compliqué, la syntaxe n'est pas claire du tout pour moi et il n'y a pas de documentation par commandes, ou alors je n'ai pas trouvé
Je suis en train de lire linéairement le tutoriel "Theorem proving in Lean", et je n'en suis pas encore arrivé aux structures et aux classes, donc je ne peux pas encore te répondre sur ce point.
Concernant la différence entre $(x:X)$, $[x: X]$ et $\{x: X\}$, de ce que j'en ai compris, la différence est la suivante:
$(x: X)$ est juste un $x$ de type X.
$[x:X]$, est une liste à élément ne contenant qu'un seul élément, $x$, de type $X$.
$\{x: X\}$ est plus subtil: c'est quelque chose qui se met dans les définitions et théorèmes pour spécifier que le type de ce qu'on définit dépend d'un $x$ de type $X$ (jusque là, exactement comme $(x: X)$), mais que par défaut, on peut omettre ce $x$. Ça dit en gros à Lean "ne t'inquiètes pas si tu ne vois pas cet argument, et essaye de faire de ton mieux pour le retrouver à partir des autres arguments".
Je continue ma lecture et si je vois un truc sur les classes/structures, je te le dis (:D
J'ai un gros problème le forum ne supporte pas le code !
$\bullet$ Pour le accolades oui c'est ça, c'est des arguments optionnels. Disons que si tu as une fonction qui prend en paramètre $3$ ensembles et deux fonctions : Quand tu veux appeler la fonction tu n'as pas envie de spécifier $A$ $B$ et $C$ : bidule A B C f g c'est ultra lourd, tu on écrits plutôt : Ce qui permet d'écrire bidule f g. Faut a peu près que lean puisse trouver les paramètres options grace au typage !
$\bullet$ Pour class versus structure, je ne sais pas trop. Disons que ce que j'ai vu, c'est utiliser class pour modéliser une structure mathématique et les structure pour les instances.
Un exemple :
Un autre exemple
structure c'est une définition avec plusieurs champs !
Je connaissais pas non plus Visual Studio, plutôt joli et léger.
Je pense qu'à ce stade, je n'ai guère le choix, il faut que je lise Theorem Proving in Lean.
Ah, et il y a une doc au moins pour la bibliothèque mathématique: https://leanprover-community.github.io/mathlib_docs
Je fais remonter ce fil simplement pour partager quelque chose que je juge intéressant en rapport avec ce fameux logiciel Lean:
https://xenaproject.wordpress.com/2020/12/05/liquid-tensor-experiment/
C'est en anglais, je m'excuse pour celles et ceux qui ne savent pas lire l'anglais, voici un petit résumé de ce que ce billet dit.
Peter Scholze (médaillé Fields 2018) s'est récemment beaucoup investit dans ce qu'il appelle les "mathématiques condensées", et est convaincu que les objets qu'il étudie (les "ensembles condensés") devraient remplacer, dans certains cas, les espaces topologiques, qui n'ont pas toujours un comportement très agréable (je ne connais pas assez ces choses pour pouvoir dire quoi que ce soit de plus précis là-dessus). Scholze a prouvé un théorème qu'il juge d'importance cruciale dans le cadre de cette théorie (le théorème 1.1 du billet), mais, comme il l'explique dans la section 6, le détail de la preuve de ce théorème est complexe, il avoue avoir bataillé pendant plus d'un an avec ce théorème. À sa connaissance, beaucoup de gens se sont intéressés aux mathématiques condensées, mais aucun groupe de travail n'est allé explorer le détail de cette preuve. Vu l'importance du théorème, Scholze estime qu'être à 99.9% sûr n'est pas suffisant, d'autant plus qu'il avoue volontiers avoir déjà persuadé des gens, parfois experts, de choses fausses.
Scholze lance donc un "défi" aux personnes intéressées par la formalisation des mathématiques et par les vérificateurs de preuves: formaliser entièrement la preuve de son théorème, pour passer de 99.9% sûr à 100% sûr. Une fois cela fait, le théorème pourra être utilisé comme "boite noire" avec l'esprit tranquille.
Cet défi a été lancé il y a deux mois, et je ne sais pas si les choses ont avancées. À mon humble avis de personne qui s'est un peu amusé avec ce logiciel, c'est un sacré défi, les myriades de petites identifications d'apparence innocente qui sont faites dans les mathématiques de ce niveau peuvent transformer la formalisation en un véritable enfer, il faut aussi par ailleurs formaliser les théorèmes, parfois très complexes, utilisés au cours de la preuve. Kevin Buzzard (qui tient le blog du xena project) explique dans les commentaires que pour l'instant, un théorème aussi complexe n'a jamais été formalisé. Il explique que pour l'instant, des définitions d'objets complexes ont été formalisés, des théorèmes complexes portant sur des objets simples ont étés formalisés, mais que jamais de théorème complexe portant sur des objets complexes n'ont été formalisés. Réussir à formaliser ce théorème constituerait une forme de "victoire" pour les formalisateurs.
Affaire à suivre...