Les mathématiques sont hantées

• 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