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 school on the use of proof assistants in teaching will be organized (see the web page of the 1st edition here).

Date: 22 June - 3 July 2026

Venue: Institut Pascal, 530 Rue André Rivière, 91400 Orsay [access] [food options]

Sponsor:

Steering committee:

• Frédéric Blanqui (INRIA & LMF, chair of EuroProofNet)
• Patrick Massot (LMO, University Paris Saclay)
• Florent Hivert (LISN, University Paris Saclay)
• Angeliki Koutsoukou Argyraki (University of London, UK)
• Benedikt Ahrens (Delft University of Technology, Netherlands)
• Alicia Villanueva (Universitat Politècnica de València, Spain)
• Cezary Kaliszyk (University of Melbourne, Australia)
• Roussanka Loukanova (Institute of Mathematics and Informatics, Bulgarian Academy of Sciences)
• Pascal Fontaine (Université de Liège, Belgium)
• Assia Mahboubi (INRIA)
• Julien Narboux (Université Paris Cité)