Les mathématiques sont hantées

 (overreacted.io)
3 points par GN⁺ 2025-08-01 | 1 commentaires | Partager sur WhatsApp
  • Lean est un langage de programmation conçu pour formaliser les mathématiques et permettre aux mathématiciens de traiter les théorèmes mathématiques comme du code
  • Les utilisateurs rédigent des théorèmes, des preuves, des axiomes et autres sous forme de code, et les preuves progressent via un ensemble d'instructions appelé tactic
  • Il est possible de fermer provisoirement une preuve incomplète avec sorry, mais cela constitue une fausse preuve comparable au any de TypeScript
  • Si l’on ajoute de mauvais axiomes (par exemple 2 = 3), cela peut entraîner une contradiction logique et la possibilité de prouver toute affirmation
  • Lean ne tire des conclusions que sur la base des axiomes choisis et du cadre logique de preuve adopté, ce qui donne une portée cruciale au maintien de la validité mathématique

Lean : traiter les mathématiques comme du code

  • Lean est un langage de programmation spécialisé dans la formalisation des mathématiques
  • Grâce à Lean, les mathématiciens peuvent exprimer les mathématiques en code et structurer leurs théorèmes et preuves afin de les partager et de collaborer
  • Il annonce un futur où une grande partie des connaissances mathématiques humaines pourrait devenir vérifiable mécaniquement et combinable sous forme de code

Premiers pas dans les preuves Lean

  • Il est possible de déclarer un théorème simple dans Lean comme theorem two_eq_two : 2 = 2 := by sorry
  • Lorsque la preuve n’est pas entièrement terminée, on utilise sorry, mais ce n’est qu’un moyen provisoire, pas une preuve réelle
    • sorry passe la vérification de preuve de Lean, mais n’est pas logiquement fiable
  • Pour une preuve complète, on utilise des tactic comme rfl (réflexivité) afin de démontrer des égalités évidentes comme 2 = 2
  • Les résultats déjà prouvés peuvent être réutilisés dans d’autres théorèmes avec exact, ce qui met en avant la modularité

Axiomes et contradictions : quand les mathématiques sont hantées

  • Si l’on ajoute un axiome tel que axiom math_is_haunted : 2 = 3, Lean le considère comme vrai
  • Cet axiome peut ensuite être utilisé dans les preuves, et il devient même possible de démontrer des conclusions mathématiquement absurdes (par exemple 2 + 2 = 6)
  • Grâce à la tactic rewrite, on peut remplacer 2 par 3 puis terminer la preuve d’égalité avec rfl
  • Si un axiome incorrect induit une contradiction, Lean bascule dans un état où toutes les propositions deviennent démontrables (effondrement logique)
  • Historiquement, au début du XXe siècle, des paradoxes de type Russell ont conduit à des remises en question fondamentales de la base des systèmes axiomatiques
  • Ainsi, Lean montre combien le choix des axiomes est déterminant pour préserver la validité d’un système logique

Lean en tant que vérificateur de preuves

  • Si les axiomes sont bien choisis et que Lean est logiquement correct, il fournit des conclusions théoriquement fiables
  • Des égalités simples aux théorèmes extrêmement complexes (par exemple le dernier théorème de Fermat), tout y est vérifié selon les mêmes principes
  • Les grands théorèmes se construisent en accumulant de manière répétée des preuves de sous-structures, comme les branches d’un arbre qui se construit progressivement
  • En exemple, un projet de formalisation du Théorème de Fermat dans Lean est en cours, avec l’objectif de parvenir à une preuve officielle sans recours à des sorry

Le plaisir d'apprendre Lean

  • Les preuves Lean sont une combinaison créative entre code et mathématiques
  • Au début, il s’agit d’apprendre à démontrer des propositions simples, puis progressivement de construire rigoureusement une mathématique de plus en plus complexe et profonde
  • Les tutoriels officiels et les ressources communautaires (telles que Natural Numbers Game, Mathematics in Lean, etc.) sont adaptés pour démarrer
  • Avec Lean, on formalise directement sa logique et on redécouvre la beauté des idées et des raisonnements subtils
  • L’article se conclut sur le fait que Lean procure une joie particulière à certains profils de personnes, même sans raison apparente

À lire aussi

1 commentaires

 
GN⁺ 2025-08-01
Réactions sur Hacker News
  • En ce moment, je réfléchis à l’idée de réécrire des actualités ou des articles de non-fiction avec un système proche de Lean — ou Lean lui-même — en traitant chaque affirmation comme un théorème à prouver, avec des preuves qui incluent aussi des citations ; par exemple, on pourrait avoir une preuve composite du type « si trois sources que j’ai approuvées affirment que c’est vrai, alors c’est vrai », et je pense qu’il serait possible de baliser tout le document pour mettre en évidence les affirmations « prouvées » ; ce ne serait pas parfait, mais ce serait une tentative de reconstruire par la technologie la rigueur qu’assuraient autrefois les médias
    • Formaliser des affirmations en langage naturel est un domaine semé d’énormes difficultés, pour des raisons similaires à celles qui rendent l’écriture de code interagissant avec le monde réel si compliquée ; tous les concepts que nous tenons pour évidents — identité, temps, causalité, etc. — doivent être traités avec une grande précision dans le formalisme pour que les faits puissent être reliés entre eux ou même exprimés ; cela dit, le problème est vraiment fascinant ; OpenCog était un projet qui poussait cette idée jusqu’au bout, et il existe aussi un champ de recherche universitaire distinct appelé représentation des connaissances et raisonnement (KRR) ; la revue IJCAI est pleine de travaux sur le sujet, et les philosophes ont aussi développé de nombreuses logiques pour formaliser divers raisonnements sur le temps, la modalité, la probabilité, etc., mais malheureusement elles se combinent rarement facilement entre elles — sauf si cela a été résolu récemment
    • Je pense que la conviction la plus importante que nous devrions avoir à propos de l’actualité ne peut généralement pas être prouvée comme un ensemble d’énoncés absolus ; des outils qui calculent des chaînes d’inférence, comme les probabilités bayésiennes, me semblent plus adaptés ; j’ai déjà vu des outils servant à ce type d’estimation numérique
    • Après avoir étudié les maths à l’université, mon écriture non fictionnelle s’est nettement améliorée ; en lisant des essais écrits par ma SO (ma compagne) et ma petite sœur, j’appliquais une rigueur presque comme devant une preuve logique, du genre : « ici tu dis que C découle de B, mais la raison pour laquelle B découle de A manque en réalité, donc on ne peut pas dire que C découle de A » ; ça semble programmable avec des outils comme les LLM, mais leurs hallucinations — la génération d’affirmations inexistantes — en montrent clairement les limites
    • Il faut faire attention : ce type d’approche peut très facilement donner une aura d’objectivité logique à des affirmations intrinsèquement radicales ou absurdes ; les opinions politiques de Gottlob Frege, l’un des pères de la logique moderne, peuvent servir d’avertissement lien connexe
    • Je trouverais plus intéressant d’avoir un moyen de cartographier toute la structure argumentative d’un sujet donné ; par exemple, partir d’une grande question comme « Dieu existe-t-il ? », puis dérouler de façon hiérarchique les arguments pour et contre, leurs contre-arguments, puis les contre-contre-arguments ; pour chaque affirmation, des citations comme « Platon a avancé cet argument » serviraient moins de preuve que de contexte historique ; l’enjeu ne serait pas de déclarer un vainqueur, mais de construire une carte argumentative qui évite de tourner en rond sur les mêmes points
  • Je me demande si, au fond, on est en train de construire un dictionnaire de preuves qui part de quelques vérités évidentes, sur lequel toutes sortes de preuves viendraient ensuite s’empiler logiquement ; dans ce cas, les preuves supplémentaires ne seraient que des combinaisons logiques de preuves déjà existantes ; j’adorerais qu’on en fasse un jeu à la Zachtronics ! Euclidea donne un peu cette sensation dans le domaine de la trigonométrie, et ce concept d’empiler une tour de logique me paraît irrésistible ; est-ce que les mathématiques pures sont justement ça, et est-ce que les professeurs de maths pures tirent leur plaisir de l’extension de ce dictionnaire logique ? Il me semble aussi me souvenir qu’un mathématicien célèbre avait établi une liste de preuves fondamentales ; si quelqu’un sait qui ou quoi c’était, et comment cela s’appelle, ça m’intéresserait ; ce sont sans doute les axiomes
    • Il existe déjà un jeu lié à cela, même si ce n’est peut-être pas exactement ce que tu veux — et ce n’est pas un jeu pour construire toutes les mathématiques ; j’y ai joué et c’était assez amusant ; c’est justement leanprover-community/nng4, mentionné dans l’article
    • Pour répondre à « faites-en un jeu à la Zachtronics », on peut dire que les maths sont déjà ce jeu-là — c’est à moitié une blague, mais à moitié vrai ; une version jeu serait vraiment amusante ; les mathématiques pures sont bien ce genre de système ; en licence, la sensation est assez juste, puis ça change un peu quand on passe à la recherche et aux articles ; si tu veux retrouver ce côté ludique, je te recommande un manuel d’algèbre abstraite comme Dummit and Foote ; il y a un vrai plaisir de jeu dans les preuves, et pour les ouvrages célèbres on trouve souvent des corrigés en ligne quand on bloque
    • Tu parles peut-être des axiomes d’Euclide, un système où sont définis des concepts comme les points, les lignes, les plans, les parallèles ; sur une sphère plutôt que sur un plan, ce système ne tient plus ; ou alors tu fais référence à la théorie des ensembles de Zermelo-Fraenkel (ZF/ZFC), sur laquelle repose toute la mathématique moderne
    • Il y a aussi un jeu appelé Bombe, une variante du démineur ; au lieu d’ouvrir directement les cases, on y joue en construisant des règles du type « dans telles conditions, on peut poser un drapeau » ; plus on avance dans les niveaux, plus les règles s’enchaînent comme des lemmes ; et à mesure que le niveau du joueur augmente, on peut même lever certaines contraintes de l’outillage pour généraliser lien du jeu
    • Les mathématiques consistent essentiellement à partir d’axiomes pour en déduire des conclusions ; bien sûr ce n’est pas toute l’histoire, mais à mon niveau c’est ainsi que je les comprends
  • Je chipote un peu, mais dire que le théorème two_eq_two ressemble à une fonction me paraît étrange ; comme il n’a pas d’arguments, il ressemble davantage à une constante — même si, oui, une constante est aussi une fonction sans arguments ; il me semblerait plus convaincant de montrer quelque chose comme ci-dessous avec x_eq_x, puis de l’appliquer comme une fonction dans 2_eq_2 
    theorem x_eq_x (x:nat) : x = x := by
  rfl

theorem 2_eq_2 : 2 = 2 := by
  exact (x_eq_x 2)
    Ici, x_eq_x ressemble bien à une fonction, et c’est effectivement ainsi qu’il est utilisé dans 2_eq_2
    • C’est une remarque juste ! Si je ne l’ai pas fait ainsi, c’est parce que la façon dont Lean gère les arguments — notamment des concepts comme les dependent types, où donner x renvoie une preuve de x = x — m’est encore un peu étrangère, et cela mérite un traitement à part entière ; j’en parlerai dans un prochain article
  • La difficulté que j’ai ressentie en apprenant Lean, c’est que les tactics (rfl et autres) sont trop englobantes, et qu’il est difficile d’en saisir le sens exact même avec les tutoriels ; par exemple, en C on peut suivre les changements d’état jusqu’au niveau des bits, alors qu’avec Lean tout me semble plus flou ; et la syntaxe de la tactic rewrite (rw) ne me paraît pas naturelle
    • Même dans Coq — désormais Rocq — j’ai toujours eu du mal à m’adapter aux tactics ; par exemple, j’avais A = B et P(A,A) et je voulais passer à P(A,B), mais rewrite ne marchait pas pour des raisons difficiles à expliquer — sans doute à cause d’une définition structurelle intermédiaire ; à l’inverse, Metamath et la base de données set.mm imposent des preuves entièrement concrètes, sans tactics du tout, avec uniquement des règles d’inférence comme ax-mp ; mais ce n’est pas simple non plus, parce qu’il faut alors mémoriser tout un ensemble de lemmes utilitaires
    • C’est l’une des raisons pour lesquelles je préfère Agda ; Agda n’a pratiquement pas de tactics, et l’on écrit directement des termes de preuve dans un langage de programmation fonctionnelle via la correspondance de Curry-Howard ; en revanche, si l’on néglige l’abstraction et la création de fonctions, même les choses triviales deviennent absurdement pénibles, donc cela demande de la discipline
    • Au moins dans Lean, on peut aller voir les définitions des tactics avec « go to definition » pour comprendre leur fonctionnement interne ; quand on apprend, la quantité de choses est écrasante, mais au bout du compte tout est inspectable — même si, lorsqu’on remonte jusqu’à la théorie des types de base, l’intuition se brouille ; et puisque tu dis que la syntaxe de rewrite ne te paraît pas naturelle, je serais curieux de savoir à quoi ressemblerait, pour toi, une syntaxe naturelle
    • Ce que j’ai trouvé intéressant, c’est que les tactics sont entièrement du code « niveau utilisateur », en dehors du kernel de preuve ; c’est logique, puisqu’on veut garder un petit kernel vérifié et ne pas le modifier ; mais cela signifie aussi que des proofs existantes peuvent casser quand les tactics changent ou évoluent ; je me demande dans quelle mesure c’est un vrai problème en pratique
    • Contrairement à ce que j’imaginais, je pensais qu’en Lean la reflection et rewrite seraient plus fondamentales que l’addition ; Lean fournit l’addition de base, mais on a quand même l’impression qu’il faut écrire rfl ou rewrite à chaque fois ; il existe peut-être dans Lean une sorte de prelude qui automatise davantage cela
  • Je me demande s’il existe une manière de lire les proofs dans Lean de façon non interactive ; en jouant au natural number game, j’ai trouvé les proofs difficiles à lire parce qu’elles se réduisaient à des suites de commandes du type rw [x] ; on peut bien voir l’état ligne par ligne dans l’éditeur, mais devoir cliquer sans cesse casse le fil ; ce serait pareil en Python si on ne voyait pas l’indentation et la structure des blocs, et qu’il fallait cliquer pour comprendre ; cela vient peut-être du nombre limité de commandes en début de jeu, mais je me demande si, dans un environnement Lean complet, la lecture devient plus fluide

    • Existe-t-il une manière de lire les preuves dans Lean de façon non interactive ?
      Je me suis posé la même question récemment et j’ai cherché un peu ; le blog lean-in-latex propose une façon de suivre ce fil en dehors de l’éditeur, sans cliquer, et montre aussi comment la communauté Lean aborde cela

    • Rocq avait autrefois quelque chose appelé « mathematical proof language » ; il est difficile de trouver des exemples réels d’usage, mais cela ressemblait à ceci 
      Lemma foo:
  forall b: bool, b = true -> (if b then 0 else 1) = 0.
proof.
  let b : bool.
  per cases on b.
    suppose it is true. thus thesis.
    suppose it is false. thus thesis.
  end cases.
end proof.
Qed.
      Cette approche rendait la lecture plus proche d’une « preuve rédigée à la main » dans un article ; elle a toutefois presque disparu faute d’usage ; le langage de preuves Isar d’Isabelle est similaire, et même plus proche du style standard ; par exemple : 
      lemma "map f xs = map f ys ==> length xs = length ys"
proof (induct ys arbitrary: xs)
  case Nil thus ?case by simp
next
  case (Cons y ys) note Asm = Cons
  show ?case
  proof (cases xs)
    case Nil
    hence False using Asm(2) by simp
    thus ?thesis ..
  next
    case (Cons x xs’)
    with Asm(2) have "map f xs’ = map f ys" by simp
    from Asm(1)[OF this] ‘xs = x#xs’‘ show ?thesis by simp
  qed
qed
      Toute la structure logique et les résultats intermédiaires y sont explicitement indiqués, et l’on peut n’abréger avec by ... que les détails où les tactics sont pertinentes ; je ne sais pas si Lean a quelque chose d’équivalent, mais cela peut au moins fournir des mots-clés de recherche ou des idées de questions à poser sur le forum Lean
    • Excellente question ! Je suis encore débutant, donc prends ça avec prudence, mais voici mon ressenti ; après avoir utilisé Lean pendant quelques mois, lire du code de preuve ne ressemble pas à lire du code de programmation : c’est plus proche d’un « balayage visuel » ; on regarde la structure générale de l’argument, les tactics utilisées, les lemmes invoqués ; dans le style réel du code Lean, on indente à chaque nouveau goal, puis on revient en arrière quand ce goal est résolu ; la forme générale de l’argument — son « shape » — compte donc beaucoup à la lecture ; voir par exemple ma PR ; à mesure qu’on s’habitue aux tactics, on reconnaît qu’un intro signifie l’entrée dans un quantificateur, qu’un constructor signifie une division du goal, etc. ; au fond, les tactics sont des macros ou une DSL qui construisent un arbre de preuve (term tree) ; quand je lis ce code, j’ai l’impression de regarder des opérations sur un arbre — découper des branches, remplir des emplacements dans un certain ordre, etc. ; il reste vrai que, pour connaître précisément les assertions intermédiaires, il faut encore cliquer ; mais une bonne preuve, fondée sur une bonne idée, peut se lire de façon aussi claire qu’un développement logique dans un article ; ceux qui veulent transmettre leur intention choisissent donc des noms lisibles, un déroulé clair, extraient de petits lemmes, et commencent par énoncer les hypothèses avant de les résoudre avec un code de preuve court ; inversement, les parties fastidieuses pour la machine mais évidentes pour un mathématicien sont souvent « golfées » ; ce style golf raccourcit souvent le code tout en ne traitant que les points que l’humain voit intuitivement ; en résumé, la structure de lecture dans Lean est implicite, mais on peut la rendre plus claire, et plus on maîtrise les tactics, plus on perçoit cette structure sans cliquer ; souvent, il suffit même de parcourir les noms des lemmes pour saisir le flux général et reconstruire facilement l’ordre
  • Le contenu était vraiment excellent ; je pense qu’il est rare de trouver quelqu’un capable d’expliquer cela d’une manière aussi digeste ; le secret, c’est de montrer toutes les petites étapes que les experts escamotent d’habitude
    • Merci !
  • Je me demande si l’on pourrait avoir dans ce fil des avis sur l’avenir de Lean par rapport à Idris/Coq/Agda ; j’aimerais étudier la représentation des connaissances, mais avant de m’engager dans une direction je m’inquiète de la taille des communautés et du risque à long terme ; j’ai déjà investi du temps autrefois dans clojure core.logic, et j’ai été refroidi par le faible intérêt et la petite taille de la communauté, donc j’hésite à me lancer trop facilement
    • D’après mon expérience, Lean et Coq/Rocq sont bien plus utilisés qu’Idris ou Agda, et disposent de bibliothèques et de communautés bien plus importantes ; Rocq est surtout très utilisé pour la vérification de programmes, probablement parce qu’il a plus d’ancienneté et quelques particularités, mais Lean pourrait bien le rattraper ; Lean est le plus courant pour la démonstration de théorèmes mathématiques ; parmi les projets célèbres de Rocq, on peut citer CompCert, CertiCoq, sel4, et il y a aussi des usages réels dans la vérification de logiciels aéronautiques (voir cette liste de projets) ; côté Lean, il y a mathlib (une collection de preuves mathématiques), la preuve du dernier théorème de Fermat (projet FLT), PFR et d’autres grands projets ; à ma connaissance, Idris et Agda n’ont pas vraiment de projets « du monde réel » comparables, même si je peux me tromper ; bien sûr, toutes ces communautés restent minuscules comparées à celles de langages comme C++ ou JavaScript, et en pratique la vérification de programmes est un travail très lent et plutôt rébarbatif ; il y aura peut-être un changement fondamental un jour avec les progrès de l’IA, mais les compétences acquises resteront probablement utiles
    • Je pense honnêtement qu’il ne faut pas voir cela comme un pari ; en pratique, la majorité des mathématiciens s’intéressent peu à la formalisation, parce qu’il existe un grand écart entre les preuves écrites à la main et la syntaxe rigoureuse exigée par un ordinateur ; il faut surtout l’aborder comme quelque chose d’amusant à apprendre et à pratiquer ; en termes de dynamique actuelle, Lean semble effectivement le plus actif ces derniers temps, mais chacun de ces outils a aussi sa base d’utilisateurs de longue date, donc il est difficile de prédire l’avenir
  • Je me demande si, sans technique particulière ni astuce, on pourrait obtenir des découvertes intéressantes simplement en lançant des choses au hasard dans Lean et en regardant ce qu’il accepte ; ou bien s’il serait possible d’automatiser cela avec un système automatique ou un LLM pour essayer à grande échelle toutes sortes de proofs ou de théories obscures et voir ce qui passe ; la question est peut-être maladroite, je comprends à peine Prolog
    • En tant que personne qui fait du certified programming comme métier, je pense que l’IA générative et les méthodes formelles sont faites pour très bien s’accorder ; à mes yeux, la question de savoir si les LLM remplaceront les programmeurs dépendra en grande partie de leur capacité à faire du certified programming et du raisonnement combinatoire,

      obtient-on des découvertes intéressantes en lançant des choses au hasard ?
      Les anciennes approches d’IA marchaient bien pour des problèmes à faible espace d’états comme les dames ; les échecs sont déjà plus difficiles, et le go est quasiment impossible pour l’IA non fondée sur l’apprentissage automatique ; les langages formels ont un espace de possibilités et un nombre d’états explorables absolument gigantesques ; si la nature du problème est bien définie, on peut faire du brute force avec un SMT solver ; à l’origine, les SMT solvers et les proof assistants relevaient de sous-domaines différents des méthodes formelles, mais désormais ils deviennent complémentaires (voir Sledgehammer, Lean-SMT)
      et si l’on faisait essayer à un LLM ou à un système automatique des proofs ou théories arbitraires ?
      Ce n’est pas encore tout à fait un sujet de recherche grand public, mais beaucoup de travaux existent ; il y avait déjà d’importants financeurs bien avant la vague LLM ; on peut citer d’anciennes tentatives comme « Learning to Find Proofs and Theorems by Learning to Refine Search Strategies », et des travaux plus récents comme DeepSeek-Prover ; on ne sait pas encore clairement comment entraîner ces systèmes ni jusqu’où leur potentiel peut aller,
      En pratique, les LLM actuels restent encore faibles dans les langages Rocq et Lean, et lorsqu’ils donnent une mauvaise réponse, la corriger est extrêmement pénible ; malgré tout, je m’attends à ce que le niveau des outils d’IA progresse fortement avec le temps

    • C’est vraiment un domaine de recherche et d’expérimentation très actif !
      La communauté Lean se retrouve beaucoup sur Zulip, et tu peux consulter divers fils de discussion utiles sur le canal Machine-Learning-for-Theorem-Proving
  • En venant d’alphaproof, qui m’a donné pour la première fois envie de m’intéresser à Lean, j’ai trouvé cet article d’introduction excellent ; pourrais-tu raconter un peu ce que tu fais avec Lean ?
    • Pour l’instant, j’étudie simplement les maths avec Lean ; plus précisément, je suis le manuel Lean de Tao, en remplissant moi-même les trous sorry laissés dans les exercices (mes solutions sont ici)
  • Je me demande si Lean a un mode de vérification qui empêche automatiquement l’usage de preuves non fiables (proof avec sorry) ou l’ajout continu de nouveaux axiomes ; par exemple, peut-on vérifier qu’« une proof n’utilise en aucune manière sorry » ou qu’elle « ne dépend que d’un ensemble fixé d’axiomes » ?
    • Il me semble que l’exemple #print axioms some_theorem mentionné vers la fin de l’article répond à cela, non ? Cela permet de voir si la preuve dépend directement ou indirectement de sorry ou d’axiomes non examinés
    • Avec print axioms, on peut vérifier qu’aucun axiome supplémentaire n’a été ajouté ; et on peut aussi regarder si cela compile sans warning ni erreur ; l’utilitaire SafeVerify détecte également certaines astuces trouvées par des systèmes de RL
    • On peut aussi faire cela avec des macros, comme expliqué ici