Formalisation Mathématique en Lean
Résumé
Après une introduction générale aux mathématiques assistées par ordinateur, je me concentrerai sur l’assistant de preuve Lean et sur sa bibliothèque de mathématiques formalisées Mathlib. Je montrerai des exemples plus ou moins élémentaires et je parlerai de quelque projet qui s’est développé, ou est en train de se développer, autour de Mathlib. Je terminerai en mentionnant le rôle que l’IA a dans cette histoire, avec une discussion de comment la formalisation pourrait modifier notre approche aux mathématiques dans le années qui viennent.
75005 Paris
Formalisation Mathématique en Lean
Après une introduction générale aux mathématiques assistées par ordinateur, je me concentrerai sur l’assistant de preuve Lean et sur sa bibliothèque de mathématiques formalisées Mathlib. Je montrerai des exemples plus ou moins élémentaires et je parlerai de quelque projet qui s’est développé, ou est en train de se développer, autour de Mathlib. Je terminerai en mentionnant le rôle que l’IA a dans cette histoire, avec une discussion de comment la formalisation pourrait modifier notre approche aux mathématiques dans le années qui viennent.