FMPSI'26 is a 2-weeks meeting aiming at gathering experts in formal mathematics or proof systems interoperability in order to discuss recent advances and make concrete progress on the formalization of advanced mathematics, the management of collaborative development of large libraries of proofs, the certification of proofs generated by automated theorems provers, the translation of definitions, theorems and proofs between different interactive theorem provers, and the use of proof assistants in teaching of mathematics, logics or computer science.
There will be 3 working groups: one on proof systems interoperability, one on formal mathematics, and one on computer algebra. The Institut Pascal will fund the accommodation of up to 6 or 7 participants in each working group. Participants will have to find their own funding for their travel to Orsay and their meals. People willing to participate and having their own funding are also welcome.
In addition, in the second week, a 2nd edition of the PAT meeting on the use of proof assistants in teaching will be organized.
Date: 22 June - 3 July 2026
Venue: Institut Pascal, 530 Rue André Rivière, 91400 Orsay [access] [hotels] [restaurants]
Organizers:
Program:
This meeting mostly consists of working sessions in small groups. Each working group will organize itself. However, every day, there will be a common short meeting with a 30 minutes talk before the afternoon coffee break. Moreover, there will be a general session at the beginning of the workshop on June 22 where every working group will have the opportunity to present its working plan, and another session at the end of the workshop on July 3 where every working group will present its results and future plans.
Offices and rooms:
Each participant will have a desk in a shared office. There are also 3 rooms for 6-8 people, 1 room for about 15 people, and 1 amphitheater of 68 people.
Schedule:
approximative daily schedule:
| time | activity |
|---|---|
| 09:00 | welcome coffee |
| 09:30 | work session |
| 12:00 | lunch |
| 13:00 | work session |
| 15:30 | talk |
| 16:00 | coffee break |
| 16:30 | work session |
special sessions:
| time | activity |
|---|---|
| Monday 22 June afternoon | one self presentation and work plan |
| Tuesday 23 June evening | cocktail |
| Thursday 25 June evening | dinner |
| Tuesday 30 June evening | cocktail |
| Thursday 2 July evening | dinner |
| Friday 3 July afternoon | restitution session |
Participants: (40 on March 6)
