WG4 Libraries of Formal Proofs

The aim of this WG is to investigate various approaches to efficiently maintain libraries of formal proofs. The goal is to make a collection of proofs that can be modified, extended, and queried by users who do not have expert knowledge of the entire collection nor of the system that was used to develop the proofs.

Activities

• 26-27 September 2024: WG1+2+4 meeting, Fontainebleau, France

• 13-14 September 2024: WG4 meeting/2nd workshop on the development, maintenance, refactoring and mining of large libraries of proofs in Tbilisi, Georgia, in co-location with ITP’24

• 26-27 September 2023: WG1+4 meeting, Fontainebleau, France

• 6-8 September 2023: Joint WG4-WG5 meeting/Workshop on Natural Formal Mathematics, and on libraries of formal proofs and natural mathematical language, Cambridge, UK

• 25-27 July 2023: Inter-WG developers meeting, Le Val d’Ajol, France

• 23-24 September 2022: WG4 kick-off meeting, Tbilisi, Georgia, at the Computational Logic Autumn Summit 2022 with the 15th Conference on Intelligent Computer Mathematics (CICM)

• 24 June 2022: Introduction to WG4 by Claudio Sacerdoti

• 24-25 June 2022: school on Dedukti and the encoding of proofs of various systems in Dedukti, and a workshop on Women in EuroProofNet, in co-location with the TYPES’22 conference at Nantes (France).