====== JNIM 2024 - Journées Nationales d'Informatique Mathématique ====== ==== Session thématique sur les assistants de preuve -- 19 mars 2024 ==== **[[#news|Actualités]] / [[#introduction|Introduction]] / [[#oratrices_et_orateurs|Oratrices et orateurs]] / [[#comite_d_organisation|Comité d'organisation]] / [[#planning_et_details_sur_la_demi-journee|Planning et détails]] ** \\ ---- À l'occasion des JNIM 2024, nous organisons une demi-journée thématique sur les assistants de preuve, à Grenoble le 19 mars 2024. ===== News ===== * Lien zoom pour participer à distance: [[https://univ-grenoble-alpes-fr.zoom.us/j/98455271867?pwd=dTNzQjM5ei9ESVo5eWVqTXdnOVVWdz09]] ===== Introduction ===== Cette demi-journée, sur la thématique des assistants de preuve, vise à partir des aspects mathématiques (logiques et algébriques) de la théorie des types pour aller jusqu'à la formalisation des mathématiques et l'usage des assistants dans l'enseignement des mathématiques et de l'informatique. La demi-journée sera principalement centrée sur l'assistant de preuve Coq (https://coq.inria.fr) mais présentera plus largement un panorama des différents assistants de preuve pour aller. Le sujet a acquis une maturité et une diffusion qui conduit à en faire une thématique inévitable pour l'IM, dans les liens qu'elle entretient en amont comme en aval entre informatique et mathématiques. Pour citer quelques uns des principaux faits marquants de la dernière décennie, on retiendra pêle-mêle: * le software system award de l’ACM en 2013 pour Coq (ainsi que le prix 2021 pour le compilateur C certifié, Compcert, prouvé en Coq); * le développement de la base de cours d’informatique en Coq [[https://softwarefoundations.cis.upenn.edu|Software foundations]] aux États-Unis; * la formalisation en Coq de la preuve du théorème de Feit-Thompson et le développement de [[https://math-comp.github.io|Mathematical Components]]; * le prix « Science ouverte du logiciel libre de la recherche 2022 » du MESRI en 2022; - le développement rapide de la bibliothèque MathLib de Lean; * la récente « liquid tensor experiment » autour des travaux de Peter Scholze; * la présence de deux exposés sur la preuve assistée par ordinateur au congrès international des mathématiciens à l’été 2022; * mais également la parution d’un article dans la gazette de la SMF sur les expériences d’[[https://www-lipn.univ-paris13.fr/~mayero/publis/Assistants_preuves_Gazette-SMF.pdf|enseignement des mathématiques avec des assistants de preuve]], etc. La pertinence de la thématique pour le GDR-IFM tient aussi au fait que les interactions entre mathématiques et informatique y prennent des formes multiples: des fondements mathématiques de ces logiciels (théorie de la démonstration, théorie de l'homotopie, ...) à ses applications comme outil servant à la production ou à la certification de mathématiques mais également comme outil pour un enseignement en mathématiques ou informatique, tout en entretenant une interaction riche avec des problématiques technologiques. En cela, la demi-journée thématique a pour objectif d'illustrer plusieurs des dynamiques entre mathématiques et informatique qui sont à l’oeuvre dans le GDR (c’est ce qui explique d'ailleurs que, si la proposition de demi-journée émane du [[https://www.irif.fr/gt-scalp/index|GT Scalp]], le thème concerne directement d'autres groupes de travail du GDR, comme LHC, ARITH et Vérif notamment). L'équipe INRIA Picube sur laquelle s'appuie principalement l'organisation de la journée est directement impliquée dans ces différents aspects; le comité d'organisation comporte en outre des membres proches, complétant les expertises. Par ailleurs, les organisatrices et organisateurs sont impliqués dans le défi [[https://liberabaci.gitlabpages.inria.fr|Liberabaci]], une action entre les équipes INRIA qui contribuent à Coq, visant à développer des contenus pédagogiques en Coq couvrant les premières années de Licence de mathématiques. Pour une prise en main rapide d'un assistant de preuve avec un objectif d'enseignement, on recommande de tester [[https://jscoq.github.io/ext/sf/|Software Foundations]] avec [[https://coq.vercel.app|jscoq]] qui permet d'exécuter directement dans un navigateur cette série de cours d'informatique intégralement formalisés en Coq, sous forme de scripts Coq à compléter, qui est largement diffusée et utilisée aux États-Unis (le [[https://softwarefoundations.cis.upenn.edu|livre original est ici]]). ===== Oratrices et orateurs ===== * Riccardo Brasca (IMJ-PRG, Université Paris Cité) * Micaela Mayero (LIPN, Université Sorbonne Paris Nord) * Julien Narboux (ICUBE, Université de Strasbourg) * Christine Paulin (LMF, Université Paris Saclay) * Pierre-Marie Pédrot (LS2N, Université de Nantes et INRIA Gallinette) * Pierre Rousselin (LAGA, Université Paris Nord) * Yannick Zakowski (LIP, Ens Lyon et INRIA Cash) ===== Comité d'organisation ===== * Emilio Gallego Arias * Hugo Herbelin * Chantal Keller * Marie Kerjean * Paul-André Melliès * Alexis Saurin ===== Planning et détails sur la demi-journée ===== ==Session 1 (14:00-16:00) Exposés invités, Chair: Chantal Keller == * **14:00: ** **Ouverture.** * **14:00-15:00:** **Exposé plénier de Christine Paulin.** //Proof Assistants : back on why and how ? // [[https://jnim2024.sciencesconf.org/530206/document|(pdf)]]
We come back on early choices made in the design of the Coq proof assistant, in term of language and architecture and in comparison with other assistants.
* **15:00-16:00:** **Exposé invité de Pierre-Marie Pédrot.** //Dans les Boyaux de mon Noyau // [[https://jnim2024.sciencesconf.org/536573/document|(pdf)]]
Dans cet exposé, nous rentrerons dans les coulisses d'un assistant de preuve basé sur la théorie des types.
Nous nous focaliserons en particulier sur les contraintes techniques résultant de ce choix de fondation, notamment au niveau de l'importance du calcul au sens large. Contrairement à l'image austère et surranée que pourrait semondre ce genre de thématique, il s'agit en fait d'un sujet bouillonant aux nombreuses conséquences aussi bien en termes de design que pour l'usage d'un tel logiciel.
* **16:00-16:30: Pause café** ==Session 2 (16:30-18:00) Table Ronde "Enseigner avec les assistants de preuve", Chair: Alexis Saurin== * **Christine Paulin.** (Université Paris Saclay) //Introduction de la table ronde// * **Yannick Zakowski.** (INRIA et ENS Lyon) //Retour d'expérience sur l'utilisation de Coq dans l'enseignement de l'informatique avec la série Software foundations// [[https://www.irif.fr/_media/users/saurin/jnim24-journee-thematique/yz.pdf|(slides)]] * **Julien Narboux.** (Université de Strasbourg) //Retour d'expériences, notamment sur un cours d'introduction à la démonstration à Strasbourg// [[https://www.irif.fr/_media/users/saurin/jnim24-journee-thematique/jn.pdf|(slides)]] * **Micaela Mayero et Pierre Rousselin.** (Université Sorbonne Paris Nord) //Retours d'expérience sur un cours de mathématiques en Coq en L1 à l'USPN et une introduction à la preuve formelle à des élèves de seconde// [[https://www.irif.fr/_media/users/saurin/jnim24-journee-thematique/mm-pr.pdf|(slides)]] * **Riccardo Brasca.** (Université Paris Cité) //Retour d'expérience sur un cours de mathématiques en Lean en L1 à UPC// * **Discussion et questions.** * **Conclusion de la table ronde.** ===== Quelques références pour aller plus loin ===== Voici des liens vers quelques références ou ressources citées lors de la demi-journée: * https://coq.inria.fr * [[https://coq.vercel.app|jscoq]], pour tester Coq dans son navigateur, sans installation préalable (exemples fournis, cf ci-dessous). * https://lean-lang.org/ * [[https://softwarefoundations.cis.upenn.edu|Software foundations]]: série de cours d'informatique intégralement formalisés en Coq, sous forme de scripts Coq à compléter. Largement diffusé et utilisé aux États-Unis. Tester [[https://jscoq.github.io/ext/sf/|Software Foundations dans votre navigateur]], grâce à [[https://coq.vercel.app|jscoq]]. * [[https://www-lipn.univ-paris13.fr/~mayero/publis/Assistants_preuves_Gazette-SMF.pdf|Article sur l'enseignement des mathématiques avec des assistants de preuve]], publié dans la gazette de la SMF * [[https://liberabaci.gitlabpages.inria.fr|Défi Liberabaci]] * [[https://hal.science/hal-04087080|Proof assistants for undergraduate mathematics education: elements of an a priori analysis]], [[https://github.com/jnarboux/PA_a_priori_analysis|videos]] * [[https://appam.icube.unistra.fr/|projet ANR Appam]] * [[https://www.math.univ-paris13.fr/~rousselin/ipf.html|Page du cours de Marie Kerjean, Micaela Mayero et Pierre Rousselin]] * [[https://www.math.univ-paris13.fr/~rousselin/enseignement.html|Stage MathsC2+ d'initiation à la preuve formelle en classe de seconde]] * [[http://jfla.inria.fr/static/slides/jfla2024-Rousselin.pdf|Présentation invitée de Pierre Rousselin aux JFLA 2024]] * [[https://moodle.u-paris.fr/course/view.php?id=41914|Page du cours de R. Brasca et A. Chambert-Loir]] * https://www.uc.pt/en/congressos/thedu/ThEdu24 * https://www.zotero.org/groups/2621881/proof_assistants_for_education/ * https://github.com/PatrickMassot/verbose-lean4 * https://github.com/impermeable/coq-waterproof * https://github.com/dEAduction/dEAduction