EuroProofNet Workshop on the development, maintenance, refactoring and search of large libraries of proofs
Warning: Time in Tbilisi (UTC+4)
Friday 23 September

12:30 CLAS lunch time

14:00 Claudio Sacerdoti (Universty of Bologna), The challenges of the EuroProofNet Working Group 4 on proof libraries

14:30 Georges Gonthier (INRIA Saclay) [online], Firstclass object hierarchies
As modern algebra is organised in hierarchies of structures, encoding these in the Coq type theory is the foundation of the Mathematical Components library and the proof of the Odd Order Theorem. As the structures and their hierarchical relations are first class objects in this encoding, it turns out the same techniques can be used to create hierarchies of other mathematical entities, such as functions, sets or relations. These have played a key part in developing a modular library in which a few overloaded lemmas can apply uniformly to a range of entities.
 15:00 Enrico Tassi (INRIA Sophia Antipolis), Hierarchy Builder, algebraic hierarchies made easy (in Coq) [online]
It is nowadays customary to organize libraries of machine checked proofs around hierarchies of algebraic structures. One influential example is the Mathematical Components library on top of which the long and intricate proof of the Odd Order Theorem could be fully formalized. Still, building algebraic hierarchies in a proof assistant such as Coq requires a lot of manual labor and often a deep expertise in the internals of the prover. Moreover, according to our experience, making a hierarchy evolve without causing breakage in client code is equally tricky: even a simple refactoring such as splitting a structure into two simpler ones is hard to get right. In this talk we describe HB, a high level language to build hierarchies of algebraic structures and to make these hierarchies evolve without breaking user code. The key concepts are the ones of factory, builder and abbreviation that let the hierarchy developer describe an actual interface for their library. Behind that interface the developer can provide appropriate code to ensure retro compatibility. We make a demo the HB language using the hierarchybuilder addon for the Coq system.

15:30 CLAS coffee break

16:00 Geoff Sutcliffe (University of Miami), The TDTP library  Tons of Data for Theorem Provers [online]
Machine Learning (ML) is emerging as a game changer in ATP, and ATP systems and tools that take advantage of ML are being developed. Concrete examples of the ways ML can be used in ATP include axiom selection, search guidance, direct logical reasoning, and learning assisted reasoning. In order to provide support for the development, evaluation, and deployment of ATP systems and tools that include ML components, the TPTP World is being extended to provide the large corpora of (ATP) data required for ML, and infrastructure to support access to and use of the data. This will be embodied in the new “Tons of Data for Theorem Provers” (TDTP) data library.

16:30 Marco Maggesi, The HOL Light library of formalized mathematics

17:00 Roland Coghetto and Julien Narboux (University of Strasbourg) [online], The GeoCoq library and its porting to Isabelle
GeoCoq is a formal proof library consisting in a formalization of foundations of geometry. It is based on several different axiom systems by Euclid, Hilbert and Tarski, and includes the arithmetization of geometry, i.e. the link between synthetic and analytic geometry. After giving a quick overview of the library, we will discuss how automation and logical foundations are used in each part of the library and the potential impact on porting the library to other proof assistants. Then, we will report on the porting of the library to Isabelle/HOL by Roland Coghetto.
 17:30 Florian Rabe (University of Erlangen), Experiences from Exporting Major Proof Assistant Libraries
The interoperability of proof assistants and the integration of their libraries is a highly valued but elusive goal in the field of theorem proving. As a preparatory step, in previous work, we translated the libraries of multiple proof assistants, specifically the ones of Coq, HOL Light, IMPS, Isabelle, Mizar, and PVS into a universal format: OMDoc/MMT. Each translation presented great theoretical, technical, and social challenges, some universal and some systemspecific, some solvable and some still open. In this talk, we survey these challenges and compare and evaluate the solutions we chose. We believe similar library translations will be an essential part of any future system interoperability solution and our experiences will prove valuable to others undertaking such efforts.

18:00 discussion session

18:30 end

19:00 dinner together in some restaurant for those who want (suggestions are welcome)
Saturday 24 September

09:00 CLAS invited speaker slot (TBA)

10:00 Reuben Rowe (Royal Halloway University of London), Refactoring OCaml

10:30 CLAS coffee break

11:00 Fabian Huch (Technical University of Münich) and Yiannis Stathopoulos (University of Cambridge), Finding facts in large formalization libraries: two Isabelle/AFP attempts

11:45 Artur Korniłowicz (University of Bialystok), XMLbased representation of Mizar Mathematical Library [online]
The Mizar Mathematical Library is a collection of mathematical papers written in the Mizar language and fully computerverified by the Mizar proof checker. From many years the Mizar Mathematical Library is a subject of translation into other systems for its crossverification or representing its content in various formats. To facilitate this task several internal XMLbased formats have been designed to be processable by generic tools independent from the Mizar system. These formats represent various syntacticsemantic information accessible at various stages of proof verification by the Mizar checker. In this talk we present constructions of the Mizar language and describe how they are represented in the XML formats. We also present the content of the Mizar Mathematical Library with a focus on its initial articles and discuss the management model of the library.

12:30 CLAS lunch time

14:00 Anne Baanen (Vrije Universiteit Amsterdam), Bundling in Dependent Type Theory
Dependent type theories allow us to bundle proofs and data in the same structure, which can be a great help for automation. On the other hand, unbundled definitions can allow greater flexibility. I discuss my experiences with refactoring between unbundled and bundled definitions in the Lean mathematical library mathlib, especially focusing on the implementation of typeclasses.
 14:45 Alexander Best (Vrije Universiteit Amsterdam), Metaprogramming for Automation of Library Maintenance
Large libraries of formal proofs are becoming increasingly common, and pose several challenges for the maintenance and upkeep if they are to be widely useful and remain so. Specific issues for maintenance include problems such as: ensuring content is not duplicated, it is organised appropriately, it is sufficiently general to be useful in other developments, or that a large library is coherent so different parts can be used together. Ensuring these properties hold is mostly done by human review, which while always a useful component can be a limiting factor of maintenance. We describe several specific problems that can be addressed with automated tooling, and give some case studies showing how automation can help humans review things they may not have the time to look into, and also help us spot difficult to notice issues.

15:30 CLAS coffee break

16:00 Riccardo Brasca (University of Paris Cité), Maintenance of Lean’s mathlib and the Liquid tensor experiment
mathlib is Lean’s mathematical library, one of the largest collection of formalized mathematics, with more than 800,000 lines of codes and 130,000 theorems/definitions. I will explain how we maintain such a big library and how new results are added every day. I will also speak about the liquid tensor experiment, a very recent project where we formally verified contemporary mathematics that used mathlib in a crucial way. Rather than focusing on the mathematics, I will explain why a centralized library is necessary for such a project.
 17:00 Talia Ringer (University of Illinois at UrbanaChampaign) [online], Concrete Problems in Proof Automation
Machine learning for proof automation has made massive strides in recent years. But are these strides in the right directions? This talk will present challenging and impactful tasks for machinelearningbased proof automation that I believe to be underexplored. It will make a case for the utility of these tasks for users of proof assistants, and the meaning of these tasks for advancing the capabilities of AI systems.
 17:30 André Freitas (University of Manchester), Natural Language & Proofs: A Neurosymbolic Perspective
This talk provides an overview of emerging methods and representation paradigms in Natural Language Processing (NLP) to support the interpretation of proofs. We will aim for a synthesis of the increasing dialogue between the neural perspective (e.g. largescale neural language models) and symbolic inference, looking into specific architectural devices which are used to integrate the properties of both types of representation. We will finalize with an argument of how these methods can support the core aims of EuroProofNet: to improve the interoperability and usability of proof systems.

18:10 end

19:00 dinner together in some restaurant for those who want (suggestions are welcome)