Séminaire « Réflexions »
The next session of the “séminaire Réflexions” will take place on Friday, September 25, in the afternoon, in the conference room at IECL-Nancy. Ghilain Bergeron and Vincent Trélat will lead a hands-on session on math in Lean (1:30–3:30 p.m.), followed by a presentation by our colleague Isabelle Dubois (IECL-Metz) on the use of proof-assisting software in teaching.
__________________________________
13h30-15h30 : session pratique « Math en Lean » préparée par Vincent Trélat (Loria) et Ghilain Bergeron (Loria)
La méthode de Héron en Lean – Un calculateur de racine carrée certifié / Heron’s method in Lean – A certified square-root calculator (https://github.com/VTrelat/Heron)
Logiciels Assistant de preuve pour enseigner la démonstration en L1 : retours d’expériences
Dans cet exposé nous partagerons :
– un retour d’expérience d’enseignement de la démonstration en mathématiques utilisant le logiciel assistant de preuve Deaduction lors de l’UE optionnelle du S2 de la L1 mathématiques à Metz
Lien vers le logiciel : https://perso.imj-prg.fr/frederic-leroux/d%E2%88%83%E2%88%80duction/
– les développements et nouveautés autour de logiciels assistant de preuve employés dans un but pédagogique et didactique en début de cursus universitaire (retours de la participation au colloque PAT 2026 https://pat2026.irif.fr/ )
