Orateur
Antoine Chambert-Loir
Description
Le développement de la librairie Mathlib au sein du logiciel de formalisation mathématique Lean vise explicitement à fournir un corpus cohérent et efficace des bases des mathématiques permettant d'y mener la formalisation de projets de recherche contemporains.Même si des projets similaires, mais moins médiatisés, existent pour d'autres logiciels,
Mathlib est souvent comparée au projet qu'avait mené Bourbaki depuis les années 1940. En mettant ces deux projets en regard, j'essayerai de dégager quelques visions philosophiques ou pragmatiques qui les sous-tendent tous deux, puis de réfléchir aux écueils qui pourraient les menacer l'un ou l'autre.