EuroProofNet Workshop on Proof Libraries

This workshop/WG4 meeting is part of the EuroProofNet Symposium. See the symposium page to get information on the other co-located events.

The objective is to have talks and demos like in the 1st Workshop on the development, maintenance, refactoring and search of large libraries of proofs and, if time permits, some common development sessions.

Date: 15-16 September 2025

Venue: Institut Pascal, 530 Rue André Rivière, 91400 Orsay [access] [hotels] [food options]

Organizers: Frédéric Blanqui, Claudio Sacerdoti, Patrick Massot

Registration/funding requests: fill in this form (registration is free but mandatory)

Important dates:

Talk/demo proposals: If you want to give a talk or make a tool demo, send a mail to Frédéric Blanqui with a title and abstract before May 25.

Speakers:

Markus Himmel (Lean FRO, Germany), the Lean standard library: development methodology and tooling

Michael Rothgang (U. Bonn, Germany), growing Lean mathlib: review and triage tooling for a large formalised mathematics library [link]

Manuel Eberl (U. Innsbruck, Austria), the Isabelle Archive of Formal Proofs [link]
Nicolas Magaud (U. Strasbourg, France), optimisation of Coq proof scripts
Cyril Cohen (Inria Lyon, France), Hierarchy Builder [github]

Mohammad Abdulaziz (King’s College London, UK), an Isabelle Library of Combinatorial Optimisation Results [github]

Julien Narboux (U. Paris Cité, France) and Pierre Boutry (U. Strasbourg, France), the Coq library on geometry [link]
Christian Merten (U. Utrech, Netherlands), algebraic geometry in Lean’s mathematical library mathlib

Sylvie Boldo (Inria Saclay, France), Numerical Analysis in Rocq – Simplicial Lagrange Finite Elements [link]

Joseph Tooby-Smith (U. Reykjavik, Iceland), PhysLean: Digitalizing Physics in Lean [link]

Yannick Forster (Inria Paris, France), the Coq Library of undecidability proofs [github]
Niels van der Weide (U. Radboud, Netherlands), the Unimath Coq library [link]
Kathrin Stark (U. Heriot-Watt, UK), Autosubst [link]
Matthieu Sozeau (Inria Nantes, France), MetaCoq [link]
Patrick Massot (U. Paris-Saclay, France), coordinating large formalization projects

Previous workshops: