In the recent years, proof assistants have shown their astounding ability to tackle the complete formalisation of large pieces of mathematics, with the celebrated certifications of the Feit-Thompson theorem, of the Kepler conjecture, and more recently, the resolution of Scholze's liquid tensor challenge.

We believe that the time is ripe to demonstrate that they can tackle mathematics in the flexible and semi-formal way it is created and exchanged by the mathematicians.

The kickoff meeting was held at the Institut Henri Poincaré on October 1-3, 2025.