Depuis septembre 2025, je suis en charge, au sein du LMBA, de la réflexion autour de la formalisation des maths, notamment via LEAN.
À ce titre, j'ai donné un exposé introductif en novembre 2025 lors du gout-thématique du LMBA, dont vous pouvez retrouver le support ici.
Le mardi 2 juin 2026, j'organise une journée consacrée à Lean et à la formalisation de preuves, ouverte à tous.
Cette journée a pour objectif de favoriser les échanges autour des usages actuels de Lean, aussi bien en enseignement qu’en recherche, et de discuter des enjeux plus larges liés à son développement, notamment en lien avec l’intelligence artificielle.
À cette occasion, Patrick Massot (Laboratoire de Mathématiques d’Orsay, Université Paris-Saclay) interviendra autour de plusieurs thématiques, parmi lesquelles:
Lean et l’enseignement,
Lean et les enjeux éthiques liés à l’usage de l’IA,
Les avancées récentes en mathématiques fondamentales permises par Lean.
D’autres interventions viendront compléter le programme.
Plus d’informations, n'hésitez pas à me contacter ou à consulter la page de l'évènement.