Universität Bonn

Workshop: Libraries of Digital Math

This workshop will focus on the organization, modularization, and curation of mathematical libraries. Contributions/talks can address any combinations of the five aspects of the Tetrapod. Though the workshop has a primary focus on formal libraries, organizational aspects of informal mathematics (e.g. via ontologies) can be addressed, if they contribute to machine-processing of the mathematical heritage.

Ilka Agricola (Philipps-Universität Marburg): A view from the IMU Committee on Electronic Information and Communication

Ilka Agricola: A view from the IMU Committee on Electronic Information and Communication

Ilka Agricola (Philipps-Universität Marburg): CEIC Publication Discussion

Ilka Agricola: CEIC Publication Discussion

Mauricio Ayala-Rincón (Universidade de Brasília): Formalization of nominal equational reasoning in PVS - nominal unification

Mauricio Ayala-Rincón: Formalization of nominal equational reasoning in PVS - nominal unification

Luis Berlioz (Universidad Nacional Autónoma de Honduras): Text mining the arXiv with LLMs

Luis Berlioz: Text mining the arXiv with LLMs

Frédéric Blanqui (INRIA): Translating HOL-Light proofs to Coq

Link to repository: https://github.com/deducteam/hol2dk

Frédéric Blanqui: Translating HOL-Light proofs to Coq

Mario Carneiro (Carnegie Mellon University): Metamath Zero - Export your Logic

Mario Carneiro: Metamath Zero - Export your Logic

Yannick Forster (Centre Inria de Paris) et al.: How libraries deal with maintenance, CI, PRs

(No recording available)

Yannick Forster (Centre Inria de Paris): The Coq library of undecidability proofs, talk with a focus how to use work around proof assistants for teaching and thesis projects

(Pending permission to publish the recording)

Thibault Gauthier (Czech Technical Unversity): Automated Alignments

(Talk given remotely)

Thibault Gauthier: Automated Alignments

Sina Hazratpour (Johns Hopkins): HoTT in Lean4

Sina Hazratpour: HoTT in Lean4

Fabian Huch (Technische Universität München): Math Libraries in ITPs

Fabian Huch: Math Libraries in ITPs

Michael Kohlhase (FAU Erlangen-Nürnberg): Flexiformal Math Libraries - Collecting/Organizing more than Def/Thm/Proof

Michael Kohlhase: Flexiformal Math Libraries - Collecting/Organizing more than Def/Thm/Proof

Heather Macbeth (Fordham University): Inequality reasoning in formalization

(No recording available)

Assia Mahboubi (Inria): Trocq - proof transfer in type theory, beyond univalence and type equivalence

(No recording available)

Florian Rabe (University Erlangen-Nuremberg): Automated Transformation of Hierarchies of Theories in Large Libraries

This talk is a teaser for the workgroup on Hierarchies of Theories

Florian Rabe: Automated Transformation of Hierarchies of Theories in Large Libraries

Florian Rabe (University Erlangen-Nuremberg): Experiences from Exporting Proof Assistant Libraries

Florian Rabe: Experiences from Exporting Proof Assistant Libraries

Aarne Ranta (University of Gothenburg): Building Grammar Libraries for Mathematics and Avoiding Manual Work

Aarne Ranta: Building Grammar Libraries for Mathematics and Avoiding Manual Work

Moritz Schubotz (FIZ Karlsruhe): Formal mathematics in zbMATH Open

Moritz Schubotz: Formal mathematics in zbMATH Open

Makarius Wenzel: Isabelle as System Platform for the Archive of Formal Proofs (AFP)

Makarius Wenzel: Isabelle as System Platform for the Archive of Formal Proofs (AFP)

Freek Wiedijk (Radboud University): From 100 to 1000+ theorems

Freek Wiedijk: From 100 to 1000+ theorems

Workgroup: Getting started with blueprint-driven formalization projects in Lean

In this working group talk, Pietro Monticone presents a tutorial showcasing how to design, manage and develop collaborative, blueprint-driven formalization projects in Lean.

Resources:

Pietro Monticone: Getting Started with Blueprint-Driven Formalization Projects in Lean