Logiciel lean

df · September 2019

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.
... 89974

nicolas.patrois · September 2019

Le code source de Lean est protégé comment ?

Math Coss · September 2019

C'est censé être open source, cf. Git hub.

df · September 2019

Le code-source est protégé par le droit d'auteur: en France du moins.
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

...

df · September 2019

Oui: c'est open-source. C'est un projet collectif et interactif. Ce qui implique une certaine souplesse quand à son utilisation.
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.
...

Héhéhé · September 2019

On est clairement à l'aube d'une révolution de la façon de faire des mathématiques. A mon avis, dans moins de 20 ans, plus aucune preuve qui [ne] sera validée formellement par un ordinateur ne sera considérée comme acceptable.

christophe c · September 2019

Je réagis à http://www.les-mathematiques.net/phorum/read.php?9,1859096,1859096#msg-1859096 :

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]

Foys · September 2019

Tu prends trop "ces gens qui font des calculs" pour des imbéciles je pense.

Héhéhé · September 2019

Je ne comprends pas ce que tu veux dire CC, quel est ton message par rapport à Lean ?

Je vous conseille la lecture de The future of mathematics ? de Kevin Buzzad.

Foys · September 2019

Héhéhé a écrit:

Je vous conseille la lecture de The future of mathematics ? de Kevin Buzzad.

Cette publicité est un peu trop agressive à mon goût. Si l'utilisation grandissante des prouveurs est une bonne chose, la mainmise d'une grosse entreprise privée sur la production mathématique mondiale est plus problématique.

Kevin Buzzad a écrit:

And now I never want to go back to pen and paper mathematics

Kevin Buzzad a écrit:

Lean is like Coq but better. So it will be able to handle these things

Je me demande combien il a touché pour dire ça.

Héhéhé · September 2019

Lean est open source, le projet est développé dans les labos de Microsoft mais rien ne t'empêche de récupérer le code source et d'en faire un fork (le code source est ici).

J'ajouterais que de nombreux contributeurs au projet sont extérieur à ce labo.

nicolas.patrois · September 2019

Sur cette page, je vois que le code source compile dans Linux et MacOS, pas dans Windows. :-D

Héhéhé · September 2019

On peut également lire A Review of the Lean Theorem Prover par Thomas Hales (la personne qui a démontré la conjecture de Kepler).

df · September 2019

Si j'en crois les critiques de Hales, "lean" n'est pas encore bien adapté à la description de structures complexes !

"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.
...

df · September 2019

Pour les logiciens et ceux qui veulent plonger corps et âme dans la théorie des systèmes formels: deux références intéressantes.
"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.

...

christophe c · September 2019

J'ajoute une remarque courte de mon téléphone concernant le fil sur lean où je rends hommage aux efforts de df pour ses liens.

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.

Héhéhé · September 2019

Ha oui ça parait crédible que les dizaines d'assistants de preuve développés par des centaines de brillants mathématiciens, logiciens et informaticiens depuis des décennies reposent tous sur une erreur de paradigme...

df · February 2020

Un exemple de formalisation sous $\textbf{Lean}$: la définition des schémas de Grothendieck.
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/
...

Chat-maths · February 2020

Le document que tu proposes est super cool df! C'est juste bien dommage qu'il ne formalise que les définitions, et aucune des preuves... J'aurais bien voulu l'utiliser pour voir un peu comment on peut faire "prouver" des trucs à Lean en pratique.

df · February 2020

En effet, pour l'instant le "travail" de Lean se résume à formaliser des définitions ou des énoncés.
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.
... 96364

df · February 2020

En théorie des catégories, voilà le festival d' "abstract nonsense" qui attend les systèmes de preuve !
... 96366

Chat-maths · February 2020

Sans demander à Lean de "produire des preuves", est-il déjà possible de lui demander d'en vérifier une si on la donne avec suffisamment de détails?

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.

df · February 2020

Je ne connais pas le système Coq mais je sais pour suivre un peu le blog XENA que beaucoup de choses ont été faites sur ce système (français comme son nom l'indique) en théorie des catégories grâce aux travaux de Gérard Huet et Amokrane Saïbi. Tu peux essayer de trouver deux écrits de ces auteurs: "Constructive category theory (CNRS)" et "Une axiomatisation constructive de la théorie des catégories (rapport de recherches de l'INRIA)".

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.
...

df · February 2020

Chat-maths: d'après ce que j'ai compris, les systèmes devraient effectivement, à termes, se coltiner de tels diagrammes !
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 !
...

umrk · February 2020

@df : merci pour le témoignage de première main de Assia Mahboubi, "priceless" comme disent les rosbeefs

Chat-maths · February 2020

Oui, merci pour le témoignage!

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 .

flipflop · March 2020

Hello,

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 ! 97724

Poirot · March 2020

Merci pour cet aperçu flipflop ;-)

flipflop · March 2020

Salut
Je vous transmets le message de quelqu'un qui travaille beaucoup sur le projet (ce n'est pas moi qui parle :-D).

" C'est juste bien dommage qu'il ne formalise que les définitions, et aucune des preuves... J'aurais bien voulu l'utiliser pour voir un peu comment on peut faire "prouver" des trucs à Lean en pratique. "

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 ?

Pour les histoires constructivisme.

Cette histoire de maths constructives n'est pas du tout obligatoire quand on utilise un assistant de démonstrations.

Héhéhé · April 2020

Pour celles et ceux qui veulent une introduction en douceur à Lean, il y a le jeu Natural Number Game qui est un "jeu" où le but est de montrer toutes les propriétés du demi-anneau $\mathbb N$. J'ai fait les premiers niveaux c'est bien foutu

Chat-maths · April 2020

Merci pour ce lien, il y a l'air d'y avoir de quoi s'amuser!

Maxtimax · April 2020

Merci Héhéhé ! Je ne sais pas si j'aurai vite le temps de m'y adonner, mais certainement un truc "ludique" pour apprendre Lean c'est une super idée.

Cere · April 2020

Super ton lien @Héhéhé
Comme quoi, on peut quasiment tout apprendre en s'amusant, c'est super !

Pour ma part, je vais essayer !

Maxtimax · April 2020

Ah par contre c'est un peu dommage, le site ne retient pas nos progrès : j'ai dû rafraîchir la page à cause d'un bug, et je n'ai pas pu revenir (il ne me restait plus qu'inequality world, j'ai un peu la flemme de devoir tout refaire jusque là!)

Héhéhé · April 2020

Je pense que tu n'as pas besoin de refaire les mondes d'avant pour accéder à un monde.

Maxtimax · April 2020

Héhéhé : ah, tu as raison ! Comme les mondes étaient indiqués en gris je m'étais persuadé qu'on ne pouvait pas y accéder :-D (trop de jeux vidéos )

Chat-maths · April 2020

Je viens de finir ce petit jeu des nombres entiers, et c'est vraiment sympathique comme truc. C'est par contre assez dommage que ce petit jeu ne montre pas du tout comment aller un peu plus loin avec ce logiciel: par exemple, programmer ses propres tactiques de preuves, il n'explique pas non plus clairement comment définir ou utiliser des structures soi-même.

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

flipflop · April 2020

Hello Chat maths
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 99682

Héhéhé · April 2020

Chat-maths: oui je suis d'accord, surtout que les documentations que j'ai trouvées sont surtout des trucs orientés computer science, il y a assez peu de ressources pour le matheux de base qui n'est pas un expert en théorie des types... C'est assez frustrant sur pas mal de choses... Je regrette que ce ne soit pas plus orienté théorie des ensembles dont on a l'habitude en maths...

flipflop: quel éditeur utilises-tu qu'on voit sur ton screenshot ?

flipflop · April 2020

Salut,

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 !

claude quitté · April 2020

Salut Flip Flop
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.

flipflop · April 2020

Coucou Claude,

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

Chat-maths · April 2020

Avant de trainer sur Zulip, je vais déjà lire un peu les deux gros tutos, histoire d'un peu comprendre de mon côté :-D

Héhéhé · April 2020

J'ai passé la soirée a essayé de faire des choses (j'étais parti sur l'idée de recoder la structure de groupe...), et je ne suis arrivé à rien. J'ai tellement de questions basiques (j'ai un peu de réserve à tout poster sur zulip) et je ne trouve aucune documentation assez éclairante...

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

structure test (E : Type) := (f : E -> E)
variables (E : Type)(F : test E)(x : E)
#check F.f x

marche alors que

class test (E : Type) := (f : E -> E)
variables (E : Type)(F : test E)(x : E)
#check F.f x

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

variables (E : Type)(G : group E)(H : group E)
variables (x : E)(y : E)
#check x*y

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é

Chat-maths · April 2020

Salut Héhéhé,

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

flipflop · April 2020

Salut

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 :

def bidule (A B C : Type) (f : A to B) (g : B to C) : A\to C := \lambda a, g  f a

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 :

def bidule {A B C : Type} (f : A to B) (g : B to C) : A\to C := \lambda a, g  f a

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.

class test (E : Type) := (f : E -> E)
variables (E : Type)(F : test E)(x : E)
#check test.f x 
 
variables (E' : Type) (y : E')
#check test.f y --- y'a pas !

Un exemple :

def  UNION (R : Type): set R to set R to  set R := \lambda A B,  A \cup B  
#print has_add
variables (R : Type)
instance : has_add(set R) :=<UNION R >    --- set R : ensemble des parties 
 
variables (A B : set R)
#check A+B       --- tu as accès a la notation +

Un autre exemple

structure Gauss := 
(a : \Z) (b : \Z) 

def I : Gauss := <0,1>

instance : has_repr (Gauss) := <\lambda z1, repr z.a ++ "+" ++ repr z.b ++ "i">   --- has_repr  et has_add c'est des classes 
instance : has_add (Gauss) ;= <\lambda z1 z2,<  z1.a+z2.a, z1.b+z2.b > >
def z0 : Gauss := < 2,3>
#eval z0+z0  --- 4 + 6i

structure c'est une définition avec plusieurs champs !

Philippe Malot · April 2020

Merci Héhéhé pour ces liens, je me suis bien amusé avec le Natural Number game, ce qui m'a donné envie d'installer lean ! :-D
Je connaissais pas non plus Visual Studio, plutôt joli et léger.

Héhéhé · April 2020

Merci pour vos réponses, j'en ai obtenu quelques unes aussi sur le chat Zulip.

Je pense qu'à ce stade, je n'ai guère le choix, il faut que je lise Theorem Proving in Lean.

Chat-maths · April 2020

Bon, j'ai fini de lire "Theorem Proving in Lean", maintenant, le fun peut commencer :-D

Ah, et il y a une doc au moins pour la bibliothèque mathématique: https://leanprover-community.github.io/mathlib_docs

flipflop · April 2020

J'admire ta capacité à lire, je suis incapable de lire plus de 5 pages d'un texte :-D

Chat-maths · February 2021

Bonjour tout le monde,

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...

Logiciel lean

Réponses

Bonjour!

Catégories

In this Discussion

Qui est en ligne 35