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 :
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 : TBA
Résume : TBA