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).

Grants

• Indexing and web search for cross libraries Proofs application
  Visitor: Abdelghani Alidra
  Host: Claudio Sacerdoti Coen
  Grant: 1413 EUR
  Dates: 2025-04-14 to 2025-04-24

• Proof mining libraries for Lean application
  Visitor: Horatiu Cheval
  Host: Thomas Powell
  Grant: 1716 EUR
  Dates: 2025-05-11 to 2025-05-17

• Centralized indexing and search for LambdaPi/Dedukti Proofs application
  Visitor: Claudio Sacerdoti Coen
  Host: Frédéric Blanqui
  Grant: 1690 EUR
  Dates: 2025-01-21 to 2025-01-30

• Indexing and retrieval of formal proofs in an heterogeneous settings application report
  Visitor: Claudio Sacerdoti Coen (Alma Mater Studiorum - Università di Bologna, Italy)
  Host: Frédéric Blanqui (Ecole Normale Superieure Paris-Saclay, France)
  Grant: 1037 EUR
  Dates: 2023-04-16 to 2023-04-21