Dear all,
Here is the current program of the event about Proof Asssitants for Teaching:
Emmanuel Beffara and Martin Bodin: Designing a tutoring system for proofs mixing both textual and visual registers.
Isabelle Dubois: Using the Proof Assistant Deaduction with First-Year Mathematics Students: A Teacher’s Report and Perspective
Within the framework of an optional course designed to improve first-year university mathematics students’ proof-writing skills, we chose to use the Deaduction software, developed by Frédéric Le Roux. This presentation highlights key aspects of this experience from the teacher’s perspective, including software usability, potential benefits and challenges, and adaptability to didactic and pedagogical objectives.
Sébastien Lahaye: A propositional logic course that is both readable and machine checked.
As part of his doctoral research, Sébastien Lahaye is investigating the use of proof assistants for teaching mathematics and computer science in preparatory classes for the French Grandes Écoles (CPGE). To begin, we focused on the chapters concerning logic. The concepts covered correspond to the CPGE MPII/MPI curriculum as well as the core CPGE curriculum: syntax and semantics of propositional logic, structural induction proof, the meta-theorem of deduction, negative, conjunctive, and disjunctive normal forms, substitution lemmas, partial valuation and the indistinguishability lemma, Quine’s algorithm, and natural deduction (proof of correctness). We developed a formalization of these concepts using the Yalep language. The goal is to create a course that is formalized, readable, and includes relatively accessible interactive proof exercises for beginners. Furthermore, to verify the library’s usability in a realistic setting, we formalized two excerpts from competitive exam questions involving logic: ENS 2024 and CCINP 2021. The current version of the course presenting the different proof states generated by Verso is available here.
Frédéric Le Roux: Deaduction
I will demonstrate Deaduction, a graphical proof assistant for undergraduate students, and explain how it is used to teach proofs to first-year students at Sorbonne Université.
Gwenaelle Leon: Discourse analysis of mathematical texts from a classic textbook in Algebra
In this presentation we will look at discourse theories used in formal linguistics and how they can be applied to mathematical texts written in natural language. In particular, we will focus on the discourse relations which are used the most in mathematical proofs. We will illustrate this analysis with a number of theorems and their proofs extracted from the textbook “Algebra” by Roger Godement. We hope that this can help us understand the connection between formal and natural language proofs in interactive theorem proving.
Patrick Massot : Teaching undergrad maths using Lean with customizable automation and controlled natural language.
Verbose Lean is a library for the Lean proof assistant whose goal is to help teaching first year undergrad students how to read and write mathematical proofs. It shares a lot of goals and principles with the Coq-Waterproof project. I will show what it looks like and emphasize the flexibility it brings to teachers. This flexibility allows to tune the amount of help given to students and the level of precision required from them.
Simon Modeste : On students’ proofs produced after using an educational proof checkers
During 4 years, we have experimented using an educational interactive proof checker in a small course in mathematics first year of university dedicated to proof, set and reasoning. In 2021-2024, we experimented the Edukera platform, that works as an online exerciser, for homeworks. In 2024-2025, we experimented practice sessions, with Deaduction, an interface for Lean developed in an educational purpose for mathematics at university. Each year students have passed a similar questionnaire, and for in the last year, students passed a mixed exam, combining proof production in Deaduction and in paper-and-pencil version. In this talk, I will present the results from the questionnaires, and some analyses of students proofs in the mixed exam, trying to understand the possible effects of the interactive proof checker on the paper-and-pencil proofs.
Cécile Ouvrier-Buffet: What proof assistants make visible: A didactic perspective on proof learning
Proof assistants are powerful tools in mathematics and computer science. From a didactic perspective, however, the key issue is not whether they are powerful, but which mathematical practices they make visible, which they hide, which they transform, and under which conditions. In this talk, I will examine proof assistants not as neutral verification tools, but as environments that reshape the way students encounter proof and proving in mathematics, taking into account three decades of international research on proof and proving in mathematics education. It raises important questions about what students actually learn, but also about how the teacher negotiates different cultures of proof, for example between proof in a proof assistant and proof in a classical pen-and-paper setting.
Gireeja Ranade: LeanTutor: Towards a verifiable natural language proof tutor
Sana Stojanović Djurdjević, Andrija Urosević and Filip Marić: Using interactive theorem proving for understanding mathematical proofs
Frédéric Tran Minh: Yalep
Now pervasive in many mathematics and computer science research domains, proof assistants have recently gained importance in education, mostly during the college years. In this talk, we propose a new learning environment as a layer above the Lean proof assistant, specially targeting high-school level proofs. Inspired by other adaptations of proof assistants for teaching such as Lean-Verbose, Coq Waterproof and Proof Buddy, we designed Yalep, a declarative controlled natural language. Our aim is to reduce the number of syntactic constructions to a minimum. Inspired by coherent logic, Yalep is based mainly on forward-chaining. We also provide convenience for type theory hiding, and functions defined on type subsets. We present the design choices and implementation of these features.
Frédéric Tran Minh: Yalep in the classroom: lessons from four experiments
From the outset, the development of Yalep—a syntactic layer over Lean for high school and undergraduate students—has been driven by classroom experimentation. We report on four experiments involving students from secondary to tertiary education, highlighting how their use of Yalep in hands-on sessions shaped our design decisions. We further assess the tool’s pedagogical benefits and limitations, and draw lessons to inform its future evolution.
Daniel J. Velleman: Two approaches to using software to teach proof: Proof Designer and How To Prove It with Lean
After some brief general remarks about the use of software to teach students about proofs, I will discuss the use of two software packages. Proof Designer is easy-to-use software that guides students through the construction of proofs in elementary set theory. How To Prove It with Lean is an online companion to the textbook How To Prove It. It explains how to use the proof assistant Lean to apply the proof-writing strategies that are taught in How To Prove It.
Jørgen Villadsen: Teaching Proof Systems and Automated Reasoning Using Isabelle
MiniCalc 2.0 is a web app designed for teaching natural deduction and sequent calculus for first-order logic with functions. The proofs can optionally be verified using the Isabelle proof assistant. We present the lessons learned from using the tool to teach computer science students about proof systems and automated reasoning. We focus on the minimal sequent calculus and briefly describe its formalization.
Burkhart Wolff: Isabelle in a Compiler Construction Class : Conception, Tooling, and Experiences
We decided to use the Isabelle Platform for the organization of the material and lab-classes in a compiler construction course at PolyTech. While proof-work is out of scope of this class, the Isabelle platform offers still a number of advantages: It is easy to install on three platforms, offers an IDE and relevant SML libraries, and can be setup to work with Lex/Yacc like tooling. Moreover, it offers the possibility for type-safe specifications of syntax-directed translations. I will present the conception of the class, the tooling and some observations from the first run of this class at PolyTech within the 4th year.