Formal Mathematics and Proof Systems Interoperability (FMPSI)

2026-06-22 09:00 2026-07-03 Formal Mathematics and Proof Systems Interoperability (FMPSI) Institut Pascal
Register / Reserve
Subjects : Mathematics

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

 

Organizers: 

 

Program Manager: Francesca Sconfienza