CIMPA School on Machine-Checked Mathematics: an introduction to formally verified mathematics
July 20th - July 31th 2026 -- Oaxaca de Juárez, Mexico
Picture courtesy of Jhovani Morales.
Description
This school aims at introducing interested mathematicians to the theory and practice of interactive theorem provers, such as Lean or Rocq (previously named Coq) and to spur collaboration between such mathematicians and current proof assistant expert users. This school targets participants with diverse backgrounds in mathematics, but without a specific knowledge in logic or program verification. The expected audience consists of curious mathematicians who have heard about the technology from recent publicity pushes (such as Peter Scholze's Liquid Tensor experiment, the verification of the Kepler Conjecture in discrete geometry, of the Odd Order theorem in finite group theory. etc.) but who have not yet tried to use a proof assistant themselves. A special emphasis will be put on the verification of computational mathematics, typically computer algebra. The event will consist of a blend of tutorials and plenary lectures, with hands- on sessions where novices will work on formalization projects alongside experts.
Program
Tentative program here.
Venue
The school will take place in facilities of the UNAM in the city center. More details will be provided shortly.
Universidad Nacional Autónoma de México, Instituto de Matemáticas, Centro Histórico Oaxaca de Juárez | Map.
Useful information
Oaxaca de Juárez, a UNESCO World Heritage Site, is one of the most beautiful mexican cities, with a vibrant cultural life.
More information about suggested accommodation coming shortly.
Registration
Deadline: 18 March 2026.
Please first refer to this page for applying to CIMPA financial support, before registering via the application website.
Confirmed lecturers
- Florent Hivert (Université Paris Saclay, France)
- Guillaume Melquiond (Inria, France)
- Florent Schaffhauser (Heidelberg Universiteit, Germany)
- Alain Chavarri Villarello (Vrije Universitet Amsterdam, The Netherlands)
- TBC
Organizers
Do not hesitate to contact the organizers for any question related to the school.
- Lucía Lopez de Medrano (UNAM) (local organizer)
- Assia Mahboubi (Inria, France)
Sponsors
This event has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No.101001995). We gratefully acknowledge the additional support of the CIMPA.
