Formal Mathematics and Proof Systems Interoperability (FMPSI'26)

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.

Lunches:

Except on Mondays, where a buffet is given at the Institut Pascal, lunches will be at the Hudi restaurant, rue Alfred Kastler 91400 Orsay, 500 m (7 minutes walk) from the Institut Pascal, preferably exactly at 12:00 or after 13:00 to avoid the queue (take your lunch ticket before going there).

Events:

time event
Monday 22 June one self presentation and work plan
Tuesday 23 June end afternoon happy hour
Thursday 25 June evening dinner
Tuesday 30 June end afternoon happy hour
Thursday 2 July evening dinner
Friday 3 July restitution session

58 participants: