Le compagnon Lean de Analysis I

 (terrytao.wordpress.com)
2 points par GN⁺ 2025-06-01 | 1 commentaires | Partager sur WhatsApp
  • Projet qui transpose dans l’assistant de preuve Lean les contenus essentiels de Analysis I, le manuel d’analyse réelle écrit par Terence Tao
  • Le projet adopte une structure bien adaptée à l’objectif de l’ouvrage original, qui met l’accent sur la construction des systèmes de nombres de base ainsi que sur la logique de la preuve et la rigueur
  • Il s’appuie sur la bibliothèque standard Mathlib, tout en incluant la construction directe des concepts fondamentaux et des exercices où les lecteurs démontrent eux-mêmes
  • Il est possible de s’exercer en remplissant soi-même les blancs (sorry) dans le code Lean ; aucune correction officielle n’est fournie, mais le projet peut être étendu via un fork
  • Utile à la fois aux débutants en Lean et aux étudiants en analyse réelle, car il permet de découvrir l’usage concret de Mathlib et de Lean

Vue d’ensemble

  • Projet open source qui recompose dans l’assistant de preuve Lean le manuel d’analyse réelle "Analysis I" écrit par Terence Tao
  • Par rapport à d’autres livres d’analyse, cet ouvrage met davantage l’accent sur le processus de construction des nombres naturels, entiers, rationnels et réels, ainsi que sur les outils de théorie des ensembles et de logique nécessaires à ce processus
  • Une grande partie du livre vise à développer une capacité de démonstration rigoureuse et systématique, ce qui le rend particulièrement compatible avec un assistant de preuve comme Lean

Caractéristiques du projet compagnon Lean

  • Il propose une "traduction" au format Lean des définitions, théorèmes et exercices de l’ouvrage original
  • Ces fichiers Lean contiennent de nombreux blancs (sorry) correspondant aux solutions des exercices, que le lecteur peut compléter lui-même pour apprendre
  • Aucune correction officielle n’est fournie, mais chacun peut forker le dépôt et créer sa propre version avec ses réponses

Lien avec Mathlib et spécificités

  • Certaines notions déjà implémentées dans Mathlib (la bibliothèque mathématique standard de Lean), comme les nombres naturels, sont volontairement reconstruites séparément à la main, puis le parcours conduit à prouver leur isomorphisme (équivalence) avec la version de Mathlib
  • Par exemple, dans Chapter2.Nat, des nombres naturels propres au projet, distincts de ceux de Mathlib, sont construits depuis zéro ; après avoir traité directement les principaux résultats, l’utilisateur s’exerce à montrer dans Lean que les deux versions sont équivalentes
  • À partir des chapitres suivants, le projet s’appuie progressivement de plus en plus sur les définitions et fonctionnalités de Mathlib

Apprentissage et usages

  • Ce compagnon Lean ne sert pas seulement à étudier l’analyse : il joue aussi le rôle d’introduction à la formalisation des mathématiques dans Lean et Mathlib
  • À la manière de "Natural number game", il comprend des exercices structurés permettant de définir et de manipuler directement des objets mathématiques dans l’environnement Lean
  • Le code lui-même peut être compilé avec Lean, mais rien ne garantit encore de façon exhaustive que tous les exercices (sorry) sont effectivement résolubles ; à ce titre, des tests pratiques et des retours sont nécessaires

Open source et contribution

  • Le dépôt est open source et peut être consulté, forké et enrichi par n’importe qui
  • Aucune solution officielle n’est fournie, ce qui permet l’existence de plusieurs versions de réponses
  • Au 31 mai, le projet a été déplacé vers un dépôt indépendant distinct

À lire aussi

1 commentaires

 
GN⁺ 2025-06-01
Commentaires sur Hacker News

  • Je trouve ça vraiment enthousiasmant, et si ce projet était déplacé vers un dépôt indépendant, il serait beaucoup plus facile à partager et à retrouver pour les autres ; j’ai toujours été curieux à propos des mathématiques, et Analysis de Tao a été le premier manuel à me montrer, d’une manière compatible avec ma façon de penser de programmeur, comment les mathématiques se construisent rigoureusement ; ensuite, je me suis aussi passionné pour Lean, mais j’ai trouvé Mathlib un peu compliqué pour apprendre les concepts mathématiques, donc j’aime beaucoup ce projet qui sert de pont entre le livre et l’outil.

    • J’ai eu une expérience similaire ; j’y ai appris la convergence, les suites de Cauchy, etc., et je me souviens que ce livre avait été publié par l’éditeur à but non lucratif indien Hindustan Book Agency, ce qui le rendait très abordable.

  • Ce qui m’enthousiasme le plus dans l’enseignement des mathématiques avec Lean, c’est le retour immédiat : si un étudiant se trompe dans une preuve, ça ne compile pas. Avant, il fallait qu’un être humain — chargé de TD, assistant ou professeur — donne ce retour, mais maintenant le compilateur Lean peut le signaler rapidement. J’aimerais qu’à l’avenir il puisse même proposer des corrections plus amicales, un peu comme le compilateur Rust (ce qui pourrait nécessiter un LLM spécialisé).

    • Je suis moi aussi globalement d’accord, mais je pense que le processus de réflexion autour d’une preuve est important. Mon expérience des maths remonte à longtemps, mais j’ai passé beaucoup de moments de « paradis mathématique » à écrire des devoirs ou des problèmes sur papier et à y réfléchir lentement. Avec Lean, j’ai peur qu’on glisse au contraire vers une approche de « tripotage » consistant à entrer des choses au hasard ou à essayer jusqu’à ce que ça passe automatiquement. J’ai aussi brièvement utilisé Coq autrefois, et j’ai le souvenir d’avoir surtout bricolé en permanence. En résumé, les assistants de preuve sont utiles à bien des égards, mais je me demande si ce lent travail de rumination ne risque pas de disparaître, en affaiblissant l’intériorisation, la conceptualisation et l’émergence d’idées nouvelles. J’aimerais bien avoir votre avis là-dessus.

  • Il existe une chaîne YouTube personnelle où l’on peut voir Terence Tao utiliser Lean directement ; je ne suis pas spécialiste du domaine, mais j’ai trouvé cela vraiment fascinant rien qu’en le regardant travailler, avec ou sans LLM (https://www.youtube.com/@TerenceTao27).

  • Je pense qu’il serait vraiment intéressant d’évaluer et de comparer l’approche traditionnelle « de manuel » avec l’approche façon Mathlib. Les bibliothèques de mathématiques formalisées ont en général l’avantage d’exprimer les résultats de la manière la plus générale possible, et il est facile d’en refactorer la structure des preuves pour les rendre élégantes. Ce refactoring est simple parce que le système suit en permanence les dépendances logiques, alors que ce n’est pas facile avec du papier et un stylo. Du coup, il est naturel de se demander s’il est pertinent d’enseigner à l’université une analyse au format « généralité maximale » comme dans Mathlib. Et cela vaut d’ailleurs pour tous les autres domaines des mathématiques fondés sur la preuve.

    • Au moins pour un cours d’introduction, je pense que ce n’est pas adapté. Il y a déjà bien trop de choses à faire entrer dans le cursus — les méthodes de preuve, les méthodes de programmation, et la théorie de base. L’expérience des enseignants qui ont vraiment essayé semble aller dans le même sens : c’est bien pour les étudiants avancés, mais pour l’étudiant moyen, c’est souvent une perte de temps.

    • En tant que mathématicien qui programme aussi depuis longtemps, je pense qu’aucune formalisation programmatique ne peut, à elle seule, donner une compréhension fondamentale. Mon biais vient du fait que j’ai appris les concepts à travers des articles. Le code est souvent accablant du point de vue de la lisibilité parce qu’il se soucie peu du style ; or des articles illisibles sont déjà difficiles, et avec le code c’est dix fois pire, car il n’y a souvent même pas de standard.

  • Je suis heureux de voir la preuve de théorèmes gagner en visibilité dans des domaines mathématiques grand public comme l’analyse. En PLT, il y avait déjà le cas célèbre du livre de Winskel The Formal Semantics of Programming Languages, formellement vérifié avec Isabelle (http://concrete-semantics.org). Si vous voulez commencer la preuve de théorèmes, je pense que ce domaine est plus facile et plus recommandable. Les théorèmes d’analyse sont de toute façon réputés assez difficiles.

    • Je ne serais pas surpris non plus que les preuves en PL aient une barrière à l’entrée plus basse. On entend souvent dire qu’il y a un aspect plus routinier — induction structurelle, application d’une induction, preuve d’invariants, répétition, ce genre de flux. Je n’ai pas beaucoup pratiqué la preuve de théorèmes, mais je n’ai jamais essayé des preuves mathématiques (surtout en analyse) avec un theorem prover. Je me demande si les preuves « mathématiques » exigent une approche très différente, et dans quelle mesure les compétences se transfèrent entre les deux. Pour référence, j’ai étudié Software Foundations en Rocq (il existe peut-être un portage Lean ?) et j’ai trouvé ça assez agréable.

  • Je pense que ce projet et cette approche conviennent très bien à un sujet fondamental comme l’analyse. Mais j’ai deux inquiétudes

    1. Les résultats centraux d’analyse dans Mathlib sont traités de manière unifiée via la notion de filtre (filter), alors que les cas particuliers sont traités séparément dans un style epsilon-delta ; je m’attends à ce que Analysis de Tao adopte une approche plus traditionnelle epsilon-delta.
    2. Mathlib est un projet qui évolue vite, donc les noms et les structures changent sans cesse ; les informations d’intégration doivent donc être entretenues en continu.

  • Je trouve ce projet vraiment formidable. Analysis I a été le premier « vrai » manuel de mathématiques que moi, ingénieur, ai réellement pu étudier jusqu’au bout, alors que j’avais échoué à plusieurs reprises avec d’autres livres (Rudin, etc.). S’il existe une version Lean, cela pourrait aider des personnes familières à la fois avec les maths et la programmation à apprendre les concepts de manière plus rigoureuse.

  • Depuis des années, il y a des tentatives de formalisation officielle de Analysis I de Tao en Lean, mais elles ont toujours eu du mal à dépasser quelques chapitres. Pendant un temps, j’ai moi-même eu envie de m’y mettre — je pensais qu’en publiant en parallèle des preuves formalisées liées au blog de solutions de Analysis I (https://taoanalysis.wordpress.com/), les personnes étudiant le livre pourraient en tirer profit. J’avais déjà partagé ce que j’avais rassemblé sur un Discord privé, mais je regroupe ici, en une seule fois, plusieurs projets Lean de référence potentiellement utiles (GitHub, gist, documentation officielle, etc.) :

  • Je me demande à quel point la « preuve d’isomorphisme avec l’objet correspondant dans Mathlib » est réellement importante. Peut-être qu’en pratique, enlever la partie isomorphisme ne changerait presque rien ? Est-ce que cela sert vraiment à quelque chose, par exemple à traduire automatiquement des théorèmes ?

    • Ces preuves d’isomorphisme

      1. permettent de démontrer que l’objet que vous avez construit et celui qui existe déjà dans Mathlib sont bien identiques ; c’est particulièrement utile quand l’objet de Mathlib est défini via une construction complexe et très généralisée, car cela aide à comprendre la différence
      2. jouent un rôle décisif pour comprendre la notation et la terminologie officielles utilisées dans Mathlib pour lire ou écrire cet objet

    • Je pense qu’il y a au minimum une valeur pédagogique : cela permet de se convaincre soi-même que l’ensemble et les opérations que l’on a construits sont bien les « mêmes » ailleurs dans le livre.

  • Je suis ravi de voir apparaître des manuels fondés sur Lean, mais pourquoi n’y a-t-il pas de HoTT (Homotopy Type Theory) ? Il existe même un article de discussion intitulé « Type Theory (HoTT) should replace (ZFC) set theory? » (https://news.ycombinator.com/item?id=43196452). Je partage aussi d’autres ressources communautaires liées à Lean vues cette semaine sur HN — « 100 theorems in Lean » (https://news.ycombinator.com/item?id=44075061), ainsi que le projet Lean de DeepMind (https://news.ycombinator.com/item?id=44119725).

    • Mais je ne vois pas vraiment pourquoi il faudrait absolument du HoTT. Les theorem provers HoTT restent peu ergonomiques, la documentation n’est pas encore suffisante, et je ne trouve pas très clair ce que HoTT apporte de plus ; à mon avis, cela n’a surtout d’intérêt que pour manipuler des structures extrêmement particulières comme celles de la théorie des catégories.

    • Comme il s’agit d’une approche de type manuel classique, la réponse à la question « pourquoi pas HoTT ? » est déjà incluse. Et puis, je pense qu’il y a aussi beaucoup d’experts sceptiques quant à son intérêt pédagogique.