This meeting is part of the Computational Logic Autumn Summit 2022.

Date: 23-24 September 2022

Venue: Tbilisi State University, Chavchavadze ave. 1, 0179 Tbilisi, Georgia

Registration: Registration is free but mandatory. To attend the workshop, physically or online, please send a mail to Frédéric Blanqui.

If you are interested in giving a talk, please send a mail to Frédéric Blanqui with a title and abstract. We welcome talks, tutorials, demos, on library descriptions or on methodologies, algorithms and tools trying to tackle the challenges raised by the development, maintenance, refactoring and search of large libraries of proofs. We especially welcome talks on search tools.

Programme: here


  • Claudio Sacerdoti (University of Bologna), The challenges of the EuroProofNet Working Group 4 on libraries
  • Fabian Huch (Technical University of Münich) and Yiannis Stathopoulos (University of Cambridge), Finding facts in large formalization libraries: two Isabelle/AFP attempts
  • Anne Baanen (Vrije Universiteit Amsterdam), Bundling in Dependent Type Theory
  • Riccardo Brasca (University of Paris Cité), Maintenance of Lean’s mathlib and the Liquid tensor experiment
  • Florian Rabe (University of Erlangen), Experiences from Exporting Major Proof Assistant Libraries
  • Alexander Best (Vrije Universiteit Amsterdam), Metaprogramming for Automation of Library Maintenance
  • Reuben Rowe (Royal Halloway University of London), Refactoring OCaml
  • Georges Gonthier (INRIA Saclay), First-class object hierarchies [online]
  • Enrico Tassi (INRIA Sophia Antipolis), Hierarchy Builder, algebraic hierarchies made easy (in Coq) [online]
  • Geoff Sutcliffe (University of Miami), The TDTP library - Tons of Data for Theorem Provers [online]
  • Artur Korniłowicz (University of Bialystok), XML-based representation of Mizar Mathematical Library [online]
  • André Freitas (University of Manchester), Natural Language & Proofs: A Neuro-symbolic Perspective
  • Marco Maggesi, The HOL Light library of formalized mathematics
  • Roland Coghetto and Julien Narboux (University of Strasbourg) [online], The GeoCoq library and its porting to Isabelle
  • Talia Ringer (University of Illinois at Urbana-Champaign) [online], Concrete Problems in Proof Automation

On site participants (21): Frédéric Blanqui, Claudio Sacerdoti, Fabian Huch, Yiannis Stathopoulos, Anne Baanen, Riccardo Brasca, Alexander Best, Reuben Rowe, Marco Maggesi, André Freitas, Maribel Fernandez, Carsten Fuhs, Peter Ölveczky, Sandra Alves, Thiago Felicissimo, Volker Stolz, Besik Dundua, Luigi Liquori, Alicia Villanueva, Ashvni Narayanan, Ramon Fernández Mir

Online participants (29): Georges Gonthier, Enrico Tassi, Geoff Sutcliffe, Artur Korniłowicz, Roland Coghetto, Julien Narboux, Florian Rabe, Talia Ringer, Christian Sottile, Georgios Pitsiladis, Dara MacConville, Adam Naumowicz, Stepan Holub, Boris Djalal, Stefania Dumbrava, Tjark Weber, Andreas Nuyts, Jørgen Villadsen, Rafael Castro Goncalves Silva, Muharrem Tuncay Gençoğlu‬, Angeliki Koutsoukou Argyraki, Yosuke Ito, Gidon Ernst, Cesare Tinelli, Michail Karatarakis, Bart Michels, Cezary Kaliszyk, Anthony Bordg, Carlos Olarte

Scientific organizers: Claudio Sacerdoti and Frédéric Blanqui

Local organizer: Besik Dundua

Funding application deadline passed. EuroProofNet can reimburse the transport to Tbilisi + 60 euros/day for the accommodation on September 23-24 for a number of participants. Please check eligibility rules and reimbursement rules to get more details.

Computational Logic Autumn Summit 2022: This meeting is part of the Computational Logic Autumn Summit 2022 which includes: