Event about the use of proof assistants for teaching in Orsay

Proof Assistants for Teaching (PAT2026) is a four-day event about the use of proof assistants for teaching proof and proving.

29 June - 3 July 2026

The event is organized in cooperation with Formal Mathematics and Proof Systems Interoperability (FMPSI’26) at Institut Pascal.

It aims to bring together researchers, teachers, students, and stakeholders interested in the use of proof assistants for teaching. PAT seeks to offer a broad spectrum of current research in the field of didactics of proof, the impact of the use of proof assistants in education, formalization of mathematics geared toward teaching, and user interfaces for theorem proving.

The objective is to gather three audiences:

  • researchers in the didactics of mathematics or informatics

  • mathematicians

  • specialists of proof assistants

How unfortunate that this is at the same dates as Rocq’n’share! Unfortunately, this may make the Rocq community a bit less represented than it should have been at this event.

This is unfortunate; I should have communicated earlier, as this Institut Pascal Program was planned two years ago.