la première séance du séminaire Réflexions qui se tiendra le vendredi 6 février 2026, de 13h30 à 17h30, dans la salle de conférence de l’Institut Élie Cartan de Lorraine, Faculté des Sciences et Technologie, Boulevard des Aiguillettes, 54506 Vandoeuvre-lès-Nancy.

Nous écouterons Patrick Massot (Laboratoire de mathématique d’Orsay)

13h30-14h45 : Présentation

Titre : Pourquoi raconter des maths aux ordinateurs ?

Résumé : Dans cet exposé j’expliquerai ce que signifie « expliquer des mathématiques à un ordinateur » et pourquoi je trouve cela intéressant et utile. Je montrerai à quoi ressemble concrètement l’utilisation d’un logiciel permettant d’encoder informatiquement des définitions, énoncés et démonstrations. Je présenterai les applications de ces techniques pour vérifier, expliquer, enseigner ou créer des mathématiques. Je mentionnerai des exemples de projets non-triviaux dans ce domaine et j’évoquerai brièvement les liens avec l’IA.

15h00-17h30: Session Pratique

Titre : Introduction à l’assistant de preuve Lean par la pratique

Le logiciel Lean permet de parler de maths de tout niveau à son ordinateur. Il peut aussi servir à enseigner le raisonnement mathématique rigoureux, par exemple en L1. Ce TP sera une introduction à l’utilisation de Lean en pratique. 

Le séminaire Réflexions est organisé conjointement par les Archives Henri Poincaré, l’Institut Élie Cartan de Lorraine et le Loria (laboratoire lorrain de recherche en informatique et ses applications). Les organisateurs pour cette année sont Alexandre Afgoustidis (IECL), Alain Genestier (IECL), Yacin Hamami (AHP) et Sophie Tourret (Loria).

The first session of the Réflexions seminar, will be held on Friday, February 6, 2026, from 1:30 p.m. to 5:30 p.m., in the conference room of the Institut Élie Cartan de Lorraine, Faculty of Science and Technology, Boulevard des Aiguillettes, 54506 Vandoeuvre-lès-Nancy.

The speaker will be Patrick Massot (Laboratoire de mathématique d’Orsay)

1:30-2:45 p.m.: Talk

Title: Why explain mathematics to computers?

Abstract: In this talk, I will explain what it means to “explain mathematics to a computer” and why I find it interesting and useful. I will show what it looks like in practice to use software that allows definitions, statements, and proofs to be encoded computationally. I will present applications of these techniques for verifying, explaining, teaching, or creating mathematics. I will mention examples of non–trivial projects in this field and briefly discuss the links with AI.

3:00-5:30 p.m.: Practical Session

Title: Introduction to the Lean proof assistant through practice

The Lean software allows you to talk about math at any level on your computer. It can also be used to teach rigorous mathematical reasoning, for example in L1. This practical session will be an introduction to the practical use of Lean.

The Réflexions seminar is organized jointly by the Archives Henri Poincaré, the Institut Élie Cartan de Lorraine, and the Loria (Lorraine Research Laboratory in Computer Science and its Applications). This year’s organizers are Alexandre Afgoustidis (IECL), Alain Genestier (IECL), Yacin Hamami (AHP) et Sophie Tourret (Loria).