After the symposium there will be a dinner for which you are welcome to join (everyone is paying for themselves).

If you would like to join the symposium and/or dinner, please register through this link, before March 13. That way we have an indication on how many people are joining.

Abstract

It has become difficult to think about a future for mathematics research that does not include Interactive theorem provers. Many mathematician are now involved in formalisation projects but also many are including Lean in their teaching.  In this talk I present some pedagogical implications of the use of Lean in teaching. In order to do so I will first discuss some findings from educational studies I have bee involved in on the impact of using Lean as part of ‘introduction to proof’ courses in first year university mathematics. I will  then draw some conclusions on the affordances and drawbacks of using this tool to support students’ transition to university mathematics and indicate some directions for future research. 

Abstract

In the first part of this talk, we will present joint work with Iro Bartzia and Antoine Meyer: an a priori analysis of the use of six different interactive proof assistants for education, based on the resolution of a typical undergraduate exercise on abstract functions. We analyze these tools according to three main categories of aspects: language and interaction mode, automation and user assistance, and proof structure and visualization.  

In the second part of the talk, I will report on our experiments using different proof assistants for teaching proof and proving and logic using Coq, Edukera, Deaduction and Verbose-Lean. 

Abstract

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. In this talk 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. 

Abstract

Joint work with Thomas Portet 

It is commonly accepted that natural numbers are one of the basic foundations of libraries for proof assistants. 

Many educators use these numbers as part of the first basic courses introducing students to theorem provers (see for example the book Logical Foundations introducing to the Rocq prover, or the number game, introducing to Lean). 

The example of Waterproof, developed in Eindhoven, shows that proof assistants can be envisioned as tools to help teaching mathematics.  Reflecting upon this goal, we came to the point of questioning the central position of natural numbers in introductory courses and we propose an introductory path where real numbers or integers are given the primary role, depending on the audience. 

We argue that in the context of teaching mathematics to newcomers, real numbers can be given the priority, and many of the practical uses of natural numbers can be recovered by considering subsets of the type of real numbers. 

We also argue that in the context of teaching proof assistants to computer science students, integers can be given the priority, and many of the practical uses of natural numbers are already provided in existing libraries. 

Abstract

Interactive Theorem Provers, also known as “Proof Assistants” allow users to state and verify complex mathematical statements. From their experimental nature in the 70s, Proof Assistants have come a long way, with many success stories among mathematicians and computer scientists. 

While Proof Assistants have been proven to be extremely helpful, they are also known for being extremely challenging to use and learn.

Owing to their roots in computer science, most proof assistants base their user interface on some variation of the “code editor” paradigm.

However, as many have noted, the “code editor” paradigm doesn’t often meet users’ expectations, in particular when catering to the needs of those that are less experienced with these systems, such as students or mathematicians.

In this talk, I will present Flèche, a new document manager for the Rocq proof assistant that aims to facilitate the task of building enhanced proof assistants. Flèche has been built taking into account extensive user and developer feedback, and provides a unique set of features and extensibility.

Flèche’s aims are twofold: we want to provide a usable, production ready platform for people willing to extend proof assistants at the document level; while at the same time developing such document managers in a rigorous, scientific way.

Abstract

A “Proof Assistant” is a computer program that allows users to create complete mathematical proofs, interactively with the computer, where the computer checks each small reasoning step. In this way one obtains the utmost guarantee of correctness. 
 
We will outline how Proof Assistants work, how they are used to verify mathematical proofs and computer systems (software and hardware). Verifying a proof with a PA is a lot of work, but as mathematical proofs get more and more difficult and complex there is an increasing use of PAs for mathematical proofs. Also for critical computer components it will pay off to verify them completely using a PA. 
 
We will discuss why one would trust a PA and their limitations in use, which basically rest on the limitations of proof automation. It has recently become clear that methods from AI, especially Machine Learning, apply very well to speeding up proof automation.