Can be followed online (see Zoom links below).
Monday 15 September
09:00-09:45 Manuel Eberl (U. Innsbruck, Austria), the Isabelle Archive of Formal Proofs
09:45-10:30 Michael Rothgang (U. Bonn, Germany), growing Lean mathlib: review and triage tooling for a large formalised mathematics library
10:30-11:00 break
11:00-11:45 Cyril Cohen (Inria Lyon, France), Hierarchy Builder
11:45-12:30 Julien Narboux (U. Paris Cité, France) and Pierre Boutry (U. Strasbourg, France), GeoCoq: a library for foundations of geometry
12:30-14:00 lunch
14:00-14:45 Christian Merten (U. Utrech, Netherlands), algebraic geometry in Lean’s mathematical library mathlib
14:45-15:30 Niels van der Weide (U. Radboud, Netherlands), the Unimath Coq library
15:30-16:00 break
16:00-16:45 Nicolas Magaud (U. Strasbourg, France), Optimization of Rocq proof scripts
16:45-17:30 Yannick Forster (Inria Paris, France), the Coq Library of undecidability proofs
17:30-18:30 happy hour
Tuesday 16 September
09:00-09:45 Joseph Tooby-Smith (U. Reykjavik, Iceland), PhysLean: Digitalizing Physics in Lean
09:45-10:30 Sylvie Boldo (Inria Saclay, France), Numerical Analysis in Rocq – Simplicial Lagrange Finite Elements
10:30-11:00 break
11:00-11:45 Kathrin Stark (U. Heriot-Watt, UK), On Autosubst: Mechanising binders in Coq
11:45-12:30 Matthieu Sozeau (Inria Nantes, France), MetaRocq: Metaprogramming and Mechanization of Rocq in Rocq
12:30-14:00 lunch
14:00-14:45 Mohammad Abdulaziz (King’s College London, UK), an Isabelle Library of Combinatorial Optimisation Results
14:45-15:30 Patrick Massot (U. Paris-Saclay, France), coordinating large formalization projects
15:30-16:00 break
16:00-16:45 Markus Himmel (Lean FRO, Germany), the Lean standard library: development methodology and tooling
16:45-17:30 Justin Asher, LeanExplore: A search engine for Lean 4 declarations (online)
Zoom links:
WG4 Monday morning - small amphi Launch Meeting - Zoom
WG4 Monday afternoon- small amphi Launch Meeting - Zoom
WG4 Tuesday morning - small amphi Launch Meeting - Zoom
WG4 Tuesday afternoon- small amphi Launch Meeting - Zoom