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] [hotels] [restaurants]
Organizers:
- general chair: Frédéric Blanqui (INRIA & LMF, chair of EuroProofNet)
- WG on interoperability: Frédéric Blanqui (INRIA & LMF, chair of EuroProofNet)
- WG on formal math: Patrick Massot (LMO, University Paris Saclay)
- WG on computer algebra: Assia Mahboubi (INRIA Nantes), Florent Hivert (LISN, University Paris Saclay)
- school: Julien Narboux (IRIF, Université Paris Cité)
Program:
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 morning | one self prnesentation 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: (29 on January 29)
-
Reynald Affeldt (Tokyo, Japan)
- Bruno Barras (Gif-sur-Yvette, France)
-
Frédéric Blanqui (Gif-sur-Yvette, France)
- Alessandro Bruni (Copenhagen, Denmark)
- Guillaume Burel (Evry, France)
-
Kevin Buzzard (London, UK)
- Mario Carneiro (Göteborg, Sweden)
-
Cyril Cohen (Lyon, France)
-
Ben Eltschig (Berlin, Germany)
- Alessio Coltellacci (Nancy, France)
-
María Inés de Frutos-Fernández (Bonn, Germany)
-
Antoine Gontard (Gif-sur-Yvette, France)
-
Florent Hivert (Gif-sur-Yvette, France)
-
Assia Mahboubi (Nantes, France)
-
Iván Martínez Comas (Gif-sur-Yvette, France)
- Patrick Massot (Orsay, France)
- Heather Macbeth (London, UK)
-
Sophie Morel (Lyon, France)
-
Julien Narboux (Paris, France)
- Oliver Nash (London, UK)
-
Michael Rawson (Southampton, UK)
- Michael Rothgang (Bonn, Germany)
-
Pierre Roux (Toulouse, France)
-
Claudio Sacerdoti Coen (Bologna, Italy)
- Kazuhiko Sakagushi (Lyon, France)
-
Geoff Sutcliffe (Miami, USA)
-
Melanie Taprogge (Greifswald, Germany)
-
Enrico Tassi (Sophia-Antipolis, France)
-
Laurent Théry (Sophia-Antipolis, France)
-
Thomas Traversié (Gif-sur-Yvette, France)
-
Théo Winterhalter (Gif-sur-Yvette, France)
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é)
