Le mardi 2 juin 2026, le LMBA 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, Benoît Cadorel (Institut Élie Cartan de Lorraine, Université de Lorraine) et Patrick Massot (Laboratoire de Mathématiques d’Orsay, Université Paris-Saclay) interviendront 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.
Les personnes intéressées sont invitées à signaler leur participation en contactant Laurine Weibel.
Programme :
9h30 - 10h30 : Exposé de Patrick Massot (LMO - Université Paris-Saclay) : Qu’apprend-t-on en racontant des maths à son ordinateur ?
11h - 12h : Exposé de Benoît Cadorel (IECL - Université de Lorraine) : Preuves assistées par ordinateur en première année de Licence : un retour d'expérience
14h - 15h30 : Exposé de Patrick Massot (LMO - Université Paris-Saclay) : Sur quelques interactions des mathématiques formalisées contemporaines
16h - 17h30/18h : Atelier en salle informatique (C306)
Titres et résumés des exposés :
Exposé de Patrick Massot (LMO - Université Paris-Saclay)
Titre : Qu’apprend-t-on en racontant des maths à son ordinateur ?
Résume : Encoder des définitions, énoncés et démonstrations mathématiques dans un langage informatique nécessite d’adapter sa façon de penser. Bien sûr il y a une adaptation de forme contrainte par la syntaxe du logiciel et les fondements logiques utilisés. Mais cet exposé se concentrera sur les aspects purement mathématiques. Je présenterai plusieurs séries d’exemples élémentaires montrant la façon dont des abstractions motivées par la formalisation permettent de simplifier des énoncés et démonstrations. Il n’y a aucun pré-requis en maths formalisées, je ne montrerai pas la moindre ligne de code informatique.
Exposé de Benoît Cadorel (IECL - Université de Lorraine)
Titre : Preuves assistées par ordinateur en première année de Licence : un retour d'expérience
Résume : Depuis septembre 2024, la maquette de la licence de Mathématiques de Nancy propose une option de Preuves assistées par ordinateur, accessible au second semestre de la L1. L'objectif visé était principalement d'utiliser LEAN comme un outil pour renforcer l'apprentissage des fondamentaux de la logique mathématique, et du sens à donner à la notion de "rigueur".
Pour plusieurs raisons, nous avons choisi de faire directement présenter le langage LEAN aux étudiant·es, en leur donnant une liste close de commandes à utiliser pour prouver quelques énoncés de base. Les séances ont essentiellement consisté en des TP durant lesquels ils et elles ont pu apprendre ces commandes, en mettant l'accent sur leur lien avec la rédaction mathématique en langage ordinaire.
Les personnes intéressées pourront retrouver tous les documents de cours ici.
J'essaierai de faire une présentation générale de mon expérience, en abordant notamment les points suivants :
Organisation générale du cours.
Comment préparer les séances de TP, que mettre dans les documents de cours ?
Evaluation.
Faut-il faire une épreuve sur machine ? sur papier ?
Intérêt pédagogique.
Comment comparer une telle option à un cours "standard", sur papier ? Que retiennent ou non les étudiant·es ?
Niveau du cours.
Le cours est-il en adéquation avec le niveau réel des étudiant·es en L1 ? Vaut-il mieux le donner une année ultérieure ?
Exposé de Patrick Massot (LMO - Université Paris-Saclay)
Titre : Sur quelques interactions des mathématiques formalisées contemporaines
Résume : En quelques années, les mathématiques formalisées sont passées d’un sujet très spécialisé et isolé à un sujet assez central par ses interactions avec l’enseignement, la recherche et l’IA. Dans cet exposé je présenterai quelques exemples de ces interactions, en insistant particulièrement sur l’enseignement et la communication entre collègues ainsi que sur les enjeux éthiques liés à l’IA.