Formal Mathematics and Proof Systems Interoperability (FMPSI’26)

FMPSI’26 is a 2-weeks program aiming at gathering experts in formal mathematics or proof systems interoperability in order to discuss recent advances and make concrete progresses on the formalization of advanced mathematics, the management of collaborative development of large library 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.

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é)