Hi everyone!
On the afternoon of March 20, there will be a mini-symposium on occasion of Jelle Wemmenhove’s PhD defense at the Eindhoven University of Technology, The Netherlands. The topic will be on proof assistants for education.
In their PhD, Jelle has been working on the educational software Waterproof (built on the Rocq prover), which aims to help students in acquiring the skill of proving mathematical statements. The mini-symposium will therefore align with the topic of Jelle’s thesis Waterproof: transforming a proof assistant into an educational tool.
The speakers are all experts in the field and members of Jelle’s doctorate committee. Some will talk about the evaluation of the use of proof assistants for education, while others will discuss the more technical aspects.
| 13:00-13:30 | Paola Iannone | Lean for teaching university mathematics |
| 13:40-14:10 | Julien Narboux | Proof assistants for undergraduate mathematics education: elements of an a priori analysis and experiment reports |
| 14:30-15:00 | Patrick Massot | Verbose Lean |
| 15:10-15:40 | Yves Bertot | Using Type Theory in an educational setting while avoiding natural numbers |
| 16:00-16:30 | Emilio Jesús Gallego Arias | TBA |
| 16:40-17:10 | Herman Geuvers | Computer Assisted Mathematical Proofs: using the computer to verify proofs |
The program and abstracts of the talks can also be found here.
The symposium will be a fully in-person event, so we realize that for many of you it will be way too far away. Nonetheless, if you are around, we would be happy with your presence. In case you would like to join the symposium, could you please register through this link, before March 13? That way we have an indication on how many people are joining.