Lean : Formaliser les mathématiques en tant que code

Lean est un langage de programmation principalement utilisé par les mathématiciens pour formaliser les mathématiques. Il permet aux mathématiciens de traiter les mathématiques comme du code, en les décomposant en structures, théorèmes et preuves, et en les partageant sur GitHub. L'article utilise un exemple simple, la preuve de 2=2, pour introduire la syntaxe de Lean et des concepts de base comme les tactiques. Il montre comment les tactiques sont utilisées pour prouver ou réfuter des affirmations mathématiques. Un axiome fictif, '2=3', illustre comment un axiome erroné peut mener à la preuve de n'importe quoi, soulignant l'importance de la vérification formelle. L'article conclut en mentionnant la formalisation en cours du dernier théorème de Fermat dans Lean comme témoignage de la puissance de Lean.