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

*(Pending permission to publish the recording)*

Video not found

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

*(Pending permission to publish the recording)*

Video not found

#### 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

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

*(No recording available)*

Video not found

#### 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)*

Video not found

#### 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)*

Video not found

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

*(No recording available)*

Video not found

#### 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

*(Pending permission to publish the recording)*

Video not found

#### 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:

- LeanProject template repository: https://github.com/pitmonticone/LeanProject
- NewLeanProject repository: https://github.com/pitmonticone/NewLeanProject
- LeanBlueprint repository: https://github.com/PatrickMassot/leanblueprint

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