Lieu de la réunion: salles 3052 et 3071, Irif, 8 Place Aurélie Nemours, Paris. L'accès est dans une zone badgée : n'hésitez pas à nous contacter en cas de besoin.
Cette réunion est en présentiel et en distanciel (voir données de connection ci-dessous).La salle 3052 est réservée tout du long, sauf entre 11h et 12h où nous serons salle 3071.
Yalep est une couche de syntaxe et d'automatisation au-dessus de Lean, rendant son usage plus adapté à l'enseignement de la preuve auprès d'élèves de lycée et de 1er cycle universitaire. Dans cette présentation nous montrerons quelques-unes de ces fonctionnalités sur des exemples de preuves au programme de seconde. Nous ferons un retour d’expérience sur une expérimentation pendant laquelle 35 élèves de Seconde ont effectué quelques preuves avec Yalep, dans le cadre d'une séquence d'une semaine (4 séances de 55 minutes) sur la démonstration conduite par leur professeur dans leur classe habituelle. Nous présenterons aussi une formalisation du programme de logique de CPGE en Yalep. L’objectif est d’obtenir un cours à la fois formalisé, lisible et avec des exercices de preuve interactifs relativement accessibles pour des néophytes. En outre, afin de vérifier l’utilisabilité de la bibliothèque dans un cadre réaliste, nous avons formalisé deux extraits de sujet de concours faisant intervenir de la logique: ENS 2024 et CCINP 2021. La version actuelle du cours présentant les différents états de preuve générée par Verso est disponible ici.
Hierarchy Builder (HB) is a high-level language for the Rocq proof assistant, designed to facilitate the declaration and hierarchy of algebraic structures. It is currently being adopted within the MathComp library as part of an ongoing effort to restructure and modularize its components. This integration effort has highlighted several usability challenges not unlinked: the underlying theory of HB is difficult to grasp and its syntax is not intuitive. This project aims to address these issues by redesigning the grammar of HB. In this talk, we present a preliminary analysis of the main usability issues, along with a set of proposed improvements. In particular, we investigate the unification of certain commands and concepts (mixins and factories), the introduction of interactive mechanisms for proof requirements, and strategies for the handling of generated names.
A universe of propositions equipped with definitional proof irrelevance constitutes a convenient medium to express properties and proofs in type-theoretic proof assistants such as Lean, Rocq, and Agda. However, allowing accessibility predicates—used to establish semantic termination arguments—to inhabit such a universe yields undecidable typechecking, hampering the predictability and foundational bases of a proof assistant. To effectively reconcile definitional proof irrelevance and accessibility predicates with both theoretical foundations and practicality in mind, we describe a type theory that extends the Calculus of Inductive Constructions featuring observational equality in a universe of strict propositions, and two variants for handling the elimination principle of accessibility predicates: one variant safeguards decidability by sticking to propositional unfolding, and the other variant favors flexibility with definitional unfolding, at the expense of a potentially diverging typechecking procedure. Crucially, the metatheory of this dual approach establishes that any proof term constructed in the definitional variant of the theory can be soundly embedded into the propositional variant, while preserving the decidability of the latter. Moreover, we prove the two variants to be consistent and to satisfy forms of canonicity, ensuring that programs can indeed be properly evaluated. We present an implementation in Rocq and compare it with existing approaches. Overall, this work introduces an effective technique that informs the design of proof assistants with strict propositions, enabling local computation with accessibility predicates without compromising the ambient type theory.
We propose to develop formal libraries of mathematics where we exploit several aspects to make the scripts closer to the structure of mathematical documents as they should be produced in a classroom. Only one type of number is being used, the type of real numbers, the subset of natural numbers is described as an inductive predicate, a new command makes it possible to define functions by recursion with inputs in the type of real numbers, but with a relevant meaning only for in the subset of natural numbers, computation with such function is also provided (but only when the outputs can derived to be an integer by code analysis), simple tactics are provided to make declarative proofs in the calculational style (only for chains of equalities), and the tactics ring and field are improved so that they can working deeply in formulas where functions exotic to the language of rings appear. To conclude, we show an example of proof where these various elements are exploited to describe pi as an infinite product of formulas that can each be described as a recursive scheme of nested square roots.
L'état actuel d'un projet d'outil pour l'enseignement de la preuve, basé sur l'utilisation d'un langage naturel contrôlé et cherchant à permettre l'association de registres textuel et visuel.
https://rendez-vous.renater.fr/Liberabaci_2026_3035b9-d3d878-b430e5
tel:0988830010,,6738029628#https://services.renater.fr/rendez-vous/rsip_pp/indexhttps://rendez-vous.renater.fr/Liberabaci_2026_3035b9-d3d878-b430e5#config.startSilent=true