# Mini-symposium on proof assistants for education

**URL:** <https://discourse.rocq-prover.org/t/mini-symposium-on-proof-assistants-for-education/2541>\
**Category:** Announcements\
**Created:** [February 27, 2025, 10:40am UTC](https://discourse.rocq-prover.org/t/mini-symposium-on-proof-assistants-for-education/2541 "2025-02-27T10:40:32Z")\
**Posts on this page:** 1\
**Page:** 1

<div class="post-metadata">

**Author:** ![jim-portegies](https://avatars.discourse-cdn.com/v4/letter/j/82dd89/32.png) [@jim-portegies](https://discourse.rocq-prover.org/u/jim-portegies)\
**Post date:** [February 27, 2025, 10:40am UTC](https://discourse.rocq-prover.org/t/mini-symposium-on-proof-assistants-for-education/2541/1 "2025-02-27T10:40:32Z")

</div>

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](https://impermeable.github.io/) (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](https://research.tue.nl/nl/publications/waterproof-transforming-a-proof-assistant-into-an-educational-too)_.

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](https://casa.win.tue.nl/home/event/mini-symposium-on-occasion-of-phd-defense-jelle-wemmenhove/).

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](https://forms.office.com/Pages/ResponsePage.aspx?id=R_J9zM5gD0qddXBM9g78ZOuWf9A0lQZJmPlgJqOkrDlUQlRMOTJNMTg0MFlaV1ZSTUE2MkkxRU9XSi4u), before **March 13**? That way we have an indication on how many people are joining.