Le compagnon Lean d’Analysis I

 (terrytao.wordpress.com)
2 points par GN⁺ 2025-06-01 | 1 commentaires | Partager sur WhatsApp
  • Terence Tao a lancé un dépôt compagnon qui transpose en code Lean les définitions, théorèmes et exercices de son manuel d’analyse réelle Analysis I
  • Par la nature du manuel, qui traite rigoureusement la construction des nombres naturels, entiers, rationnels et réels ainsi que la théorie des ensembles et la logique, il présente une structure bien adaptée à l’apprentissage avec un assistant de preuve
  • Le périmètre actuel couvre une partie du chapitre 2, la section 3.1 sur la théorie élémentaire des ensembles et la section 4.1 sur les entiers, avec aussi un isomorphisme avec les nombres naturels de Mathlib
  • Le code compile dans Lean, mais il reste de nombreux sorry, et il est recommandé de les compléter dans des forks plutôt que de publier des solutions officielles
  • Cette ressource peut servir à résoudre les exercices en Lean comme voie alternative, ainsi que d’introduction à l’usage de Mathlib au fil des chapitres

Projet de transposition d’Analysis I en Lean

  • Lean companion to “Analysis I” est un projet qui “traduit” en Lean diverses définitions, théorèmes et exercices d’Analysis I
  • Les exercices du livre peuvent aussi être résolus en complétant les sorry correspondants dans le code Lean
  • Les solutions officielles des exercices ne devraient pas être hébergées dans le compagnon, et les versions où les sorry sont remplis peuvent être créées sous forme de forks du dépôt

Pourquoi le manuel et Lean vont bien ensemble

  • Analysis I est un manuel qui se concentre davantage sur les questions fondamentales afin de compléter les manuels classiques d’analyse réelle
    • construction des nombres naturels, entiers, rationnels et réels
    • théorie des ensembles et logique permettant de développer des preuves très rigoureuses
  • Au moment de l’écriture du livre, des assistants de preuve comme Coq et Agda existaient déjà, mais la vérification formelle n’était pas alors un sujet d’intérêt
  • Après avoir expérimenté la vérification formelle par la suite, il est apparu que le contenu du livre se prête bien aux assistants de preuve
  • La théorie naïve des types utilisée implicitement dans le livre pour construire les systèmes numériques standards correspond bien à la théorie des types dépendants de Lean
  • La prise en charge des quotient types par Lean s’accorde également avec la méthode de construction du livre

Périmètre actuellement transposé en Lean

Relation avec Mathlib

  • La formalisation est conçue pour être séparée, sur certains points, de la bibliothèque mathématique standard de Lean, Mathlib, et pour dépendre de Mathlib sur d’autres points
  • Mathlib dispose déjà d’une notion standard de nombres naturels
  • Dans la formalisation Lean, on commence par développer Chapter2.Nat, qui reconstruit les nombres naturels “à la main”
    • En travaillant dans l’espace de noms Chapter2, il peut être utilisé sous le nom Nat
    • Des résultats de base parallèles aux lemmes de Mathlib sur les nombres naturels sont mis en place
    • Beaucoup de ces preuves restent des exercices pour le lecteur et sont actuellement remplacées par sorry
  • La section épilogue établit un isomorphisme entre ces nombres naturels alternatifs et les nombres naturels de Mathlib
    • Plus précisément, cet isomorphisme est lui aussi formulé comme un exercice
  • Par la suite, la construction des nombres naturels du chapitre 2 n’est plus utilisée, au profit des nombres naturels de Mathlib
  • Le projet prévoit de poursuivre ce schéma dans les chapitres ultérieurs du livre, en s’appuyant de plus en plus sur les définitions et fonctions de Mathlib plutôt que sur les constructions propres des premiers chapitres

Mode d’utilisation et état de vérification

  • Le code du dépôt compile dans Lean
  • Toutefois, il n’a pas encore été testé que les nombreux sorry présents dans le code peuvent effectivement tous être complétés
  • Il faut aussi vérifier que les lemmes auxiliaires nécessaires et l’API des fichiers Lean sont suffisants
    • L’objectif est de vérifier que les sorry peuvent être remplis de manière conceptuellement naturelle, sans dépendre de techniques obscures de programmation Lean
  • Des bénévoles sont souhaités pour playtester le compagnon et vérifier qu’il est réellement possible de résoudre les exercices dans Lean
  • Tout autre retour est également bienvenu

Un support d’introduction à Lean et Mathlib

  • Ce compagnon peut servir non seulement pour l’analyse réelle, mais aussi comme introduction à Lean et Mathlib
  • Sous cet aspect, il ressemble dans une certaine mesure au Natural number game
  • Le Natural number game recoupe largement les sujets du chapitre 2 d’Analysis I

À lire aussi

1 commentaires

 
GN⁺ 2025-06-01
Avis de Hacker News

  • Ce qui me paraît le plus intéressant quand on enseigne les mathématiques avec Lean, c’est le retour immédiat. Si la preuve d’un étudiant est fausse, elle ne compile tout simplement pas.
    Avant, il fallait qu’une personne comme un assistant, un chargé de cours ou un expert la relise pour obtenir un retour ; désormais, le compilateur Lean peut en fournir un rapidement.
    À l’avenir, j’aimerais que le compilateur Lean propose aussi des retours plus pédagogiques, comme le compilateur Rust suggère des corrections de code ; il faudra peut-être un LLM dédié.

    • Je suis presque entièrement d’accord, mais je me demande si l’apprentissage de la preuve ne risque pas d’y perdre la pensée lente.
      Autrefois, étudier les maths impliquait souvent de passer beaucoup de temps sur un devoir, à essayer diverses choses sur papier et à les ruminer longuement ; ce processus menait parfois à l’intériorisation des concepts et à de nouvelles idées.
      Avec Lean, cela pourrait devenir une manière de procéder où l’on tente des choses au hasard, on vérifie et on déverse des essais. Quand j’ai touché un peu à Coq, j’ai surtout le souvenir d’avoir bricolé et essayé toutes sortes de choses.
    • Acorn fonctionne déjà de cette manière. Quand une preuve échoue mais qu’elle est « presque correcte », il affiche dans VS Code des suggestions comme celles-ci :
      reduce(r.num, r.denom) = reduce(a, b)
      cross_equals(a, b, r.num, r.denom)
      r.denom * a = r.num * b
      Il n’utilise pas de LLM : un petit modèle local tourne dans l’extension VS Code. J’aimerais qu’un jour ce petit modèle local devienne assez puissant pour dépasser largement l’humain. Plus de détails ici : https://acornprover.org/docs/tutorial/proving-a-theorem/.

  • C’est vraiment prometteur. J’aimerais que ce soit déplacé dans un dépôt séparé, pour que ce soit plus facile à trouver et à envoyer à d’autres.
    Les mathématiques m’intéressaient déjà, mais le livre Analysis de Tao a été le premier manuel à me montrer comment les maths se construisent de façon rigoureuse, exactement comme l’esprit d’un programmeur pouvait s’y attendre.
    J’ai ensuite un peu essayé Lean, et j’y ai trouvé une satisfaction similaire, mais Mathlib était assez complexe pour apprendre des concepts mathématiques. Je suis donc heureux de voir apparaître un pont entre le livre et l’outil.

    • Moi aussi, j’ai appris dans ce livre des notions comme la convergence et les suites de Cauchy. Il était publié par Hindustan Book Agency, une maison d’édition locale à but non lucratif, donc son prix était aussi très abordable.

  • C’est agréable de voir la démonstration de théorèmes prendre de l’élan sur des sujets mathématiques grand public comme l’analyse.
    Du côté de la théorie des langages de programmation, dès le milieu des années 2010, quand les outils commençaient déjà à être assez mûrs, un manuel de référence comme The Formal Semantics of Programming Languages de Winskel a été formellement vérifié en Isabelle. Ce n’est pas une transcription complète 1:1, mais http://concrete-semantics.org en est un exemple.
    Si la démonstration de théorèmes vous intéresse, je pense personnellement que c’est un point de départ bien plus facile. Les théorèmes d’analyse sont déjà assez difficiles en eux-mêmes.

    • Que les preuves sur les langages de programmation soient plus faciles pour débuter ne me surprendrait pas. Comme les gens le disent, il semble y avoir beaucoup plus de procédures formalisées.
      On fait de l’induction structurelle, on applique l’hypothèse d’induction pour montrer que l’invariant est préservé, puis on continue ainsi.
      Je n’ai pas énormément pratiqué la preuve de théorèmes, ni fait de preuves « mathématiques » comme de l’analyse dans un assistant de preuve, mais si les preuves mathématiques demandent une approche très différente, je me demande dans quelle mesure les compétences se transfèrent entre les deux.
      Je voudrais aussi mentionner Software Foundations de Rocq. Il existe peut-être un port vers Lean, mais quand j’en ai suivi les premières parties, c’était assez agréable.

  • Il serait très intéressant d’évaluer en quoi l’approche grand public de type « manuel » diffère de celle de Mathlib.
    En général, les bibliothèques de mathématiques formalisées énoncent les résultats avec un maximum de généralité et facilitent le refactoring du développement des preuves vers quelque chose de plus intuitif et élégant.
    Le refactoring est facile parce que le système suit en permanence ce qui découle logiquement de quoi. Quand on travaille au papier-crayon, on n’a pas cela, et on manque souvent des occasions de retravailler la présentation.
    Une question naturelle est donc de savoir s’il serait pertinent d’enseigner en licence une version d’analyse réelle à la manière de Mathlib, avec une « généralité maximale ». Cela vaut bien sûr aussi pour les autres domaines des mathématiques fondées sur les preuves.

    • Pour un cours d’introduction, je pense clairement que non. Il y a déjà trop de choses à apprendre : comment prouver, comment programmer, et le contenu propre au cours.
      À ma connaissance, l’expérience des enseignants qui ont réellement essayé va dans le même sens. Cela peut convenir à des étudiants avancés, mais pour l’étudiant moyen, il y a de fortes chances que cela fasse perdre du temps de cours.
    • En tant que mathématicien qui programme aussi depuis longtemps, j’ai l’impression qu’aucun formalisme de type programme ne parviendra à transmettre la compréhension de base.
      Mon biais vient certes du fait que j’ai appris les concepts mathématiques dans des articles.
      Le code représente une surcharge énorme, et j’ai souvent l’impression qu’il ne suit généralement aucune norme de style. Pour quelqu’un qui a dû lire des articles de maths jugés incompréhensibles, le code est dix fois pire, car il n’existe quasiment aucun critère réel de lisibilité.

  • Il y a aussi quelques vidéos où Terence Tao utilise Lean sur sa propre chaîne YouTube. https://www.youtube.com/@TerenceTao27
    Je ne connais pas les détails, mais c’était intéressant de le voir travailler, avec ou sans LLM.

  • Pour un sujet fondamental comme l’analyse, je pense que c’est un très bon projet et une bonne approche.
    Deux inquiétudes me viennent tout de suite à l’esprit. Premièrement, les principaux résultats d’analyse de Mathlib utilisent la notion de filtres pour traiter les limites de manière générale et unifiée. Certains résultats sont tout de même spécialisés sous forme epsilon-delta. Je pense que l’Analysis de Tao adoptera une approche epsilon-delta plus traditionnelle.
    Deuxièmement, Mathlib évolue vite et casse souvent. Les noms changent, les refactorings se poursuivent, et un dépôt en aval aura donc besoin d’une maintenance continue.

  • C’est une idée assez radicale, mais je pense que l’enseignement des mathématiques devrait se concentrer sur la création de systèmes de calcul formel comme Mathematica et de prouveurs de théorèmes comme Lean. Il faudrait aussi y intégrer fortement la visualisation et les applications pratiques.
    Dans une version extrême, cela pourrait prendre la forme d’un apprentissage où l’on ne fait quasiment pas de mathématiques sur papier, tout en étant capable de prouver dans Lean tout ce que l’on a appris.
    Le système actuel se concentre sur d’interminables calculs manuels ; je trouve cela tellement inutile et ennuyeux que cela finit par dégoûter les gens des mathématiques.

  • Un manuel Lean, c’est une bonne chose. Mais pourquoi n’y a-t-il pas de HoTT ?
    “Should Type Theory (HoTT) Replace (ZFC) Set Theory as the Foundation of Math?”
    https://news.ycombinator.com/item?id=43196452
    Autres ressources Lean passées sur HN cette semaine :
    “100 theorems in Lean”
    https://news.ycombinator.com/item?id=44075061
    “Google-DeepMind/formal-conjectures: collection of formalized conjectures in lean” https://news.ycombinator.com/item?id=44119725

    • La formalisation de plusieurs idées de HoTT est actuellement menée dans la communauté Agda. https://martinescardo.github.io/HoTT-UF-in-Agda-Lecture-Notes/
      Les motivations précises sortent de mon domaine, donc je ne les connais pas, mais Agda semble mieux adapté que Lean pour formaliser ces idées.
      Plus tard cette année, un nouveau manuel devrait aussi paraître ; il constituera une mise à jour plus moderne du livre HoTT existant, avec également une formalisation en Agda.
      https://www.cambridge.org/core/books/introduction-to-homotopy-type-theory/0DD31EC06C80797A50ACE807251E80B6
      https://github.com/HoTT-Intro/Agda
    • HoTT est un sujet très technique et très étroit, donc cela n’a pas de sens de mener deux projets aussi ambitieux en même temps de cette façon.
      HoTT est encore loin d’être accepté comme un standard raisonnable, et pour la plupart des gens c’est un sujet qui bloque dès le départ.
      C’est un peu comme demander à un développeur de frameworks JavaScript pourquoi il n’a pas créé de framework pour Elm ou Haskell.
    • Je ne vois même pas pourquoi il faudrait HoTT.
      Il y a eu beaucoup moins de travail consacré à rendre les prouveurs de théorèmes HoTT faciles à utiliser, et la documentation est bien plus pauvre.
      Les avantages de HoTT ne sont pas clairs non plus. Il semble seulement réduire le travail quand on manipule des constructions très obscures de théorie des catégories.
    • La question « pourquoi n’y a-t-il pas HoTT ? » est un peu étrange.
      Terrence Tao a plusieurs manuels d’analyse, et ceci est un compagnon Lean pour son premier livre. Il n’a pas de manuel de théorie des types, donc il n’y a pas de théorie des types d’ordre supérieur. Ce qu’il cherche à faire est complètement différent dès le départ.
    • Le simple fait qu’il s’agisse d’un compagnon à un manuel existant répond déjà à « pourquoi pas HoTT ? ». Une autre raison pourrait aussi être que les gens doutent de sa valeur pédagogique.

  • Très chouette. Analysis I a été le premier « vrai » manuel de mathématiques que moi, ingénieur et non mathématicien, ai eu l’impression de pouvoir suivre et résoudre entièrement, après plusieurs tentatives avec d’autres livres comme Rudin.
    J’espère que le compagnon Lean le rendra plus accessible aux personnes qui sont à l’aise avec les mathématiques et la programmation, et qui veulent apprendre de façon rigoureuse.

  • Ces dernières années, il y a eu des tentatives régulières de formaliser en Lean le livre Analysis I de Tao, et certaines personnes essayaient de faire exactement ce que Tao fait maintenant. Malheureusement, la plupart n’ont pas dépassé les premiers chapitres ; Tao espère aller plus loin
    J’ai moi-même envisagé de m’y mettre. Je me disais qu’ajouter des preuves formalisées de chaque exercice sur mon blog de commentaires d’Analysis I https://taoanalysis.wordpress.com/ serait utile aux personnes qui suivent le livre
    Je l’ai aussi publié sur le serveur Discord privé du livre, mais comme cela peut également être utile ici, je partage les ressources associées
    https://github.com/cruhland/lean4-analysis — provient de https://github.com/cruhland/lean4-axiomatic
    https://github.com/Shaunticlair/tao-analysis-lean-practice
    https://github.com/vltanh/lean4-analysis-tao
    https://github.com/gabriel128/analysis_in_lean
    https://github.com/mk12/analysis-i
    https://github.com/melembroucarlitos/Tao_Analysis-LEAN
    https://github.com/leanprover-community/NNG4/ — ne suit pas le livre de Tao, mais comme il s’agit d’une version Lean4 du jeu des nombres naturels, le contenu est très proche du chapitre 2
    https://github.com/djvelleman/STG4/ — jeu de théorie des ensembles en Lean4, donc peut être similaire au chapitre 3. Cela dit, dans https://github.com/djvelleman/STG4/blob/main/Game/Metadata.lean, on voit import Mathlib.Data.Set.Basic, ce qui laisse penser qu’il importe les ensembles de Lean plutôt que de redéfinir les ensembles et d’en poser les axiomes. Cette approche peut faire que Lean en sache « trop » sur la théorie des ensembles, ce qui peut ne pas convenir à l’objectif
    https://gist.github.com/kbuzzard/35bf66993e99cbcd8c9edc4914c9e7fc — pour la construction des entiers
    https://github.com/ImperialCollegeLondon/IUM/blob/main/IUM/2023/IntegerGame.lean — c’est peut-être le même fichier que ci-dessus
    https://github.com/ImperialCollegeLondon/IUM/blob/main/IUM/2023/RationalGameAlgebra.lean — pour la construction des rationnels
    https://lean-lang.org/theorem_proving_in_lean4/axioms_and_computation.html#function-extensionality — montre une manière de définir un type Set personnalisé