50:45

Marco Caminati: Challenges in formalising recent results in formal language theory

21:56

Raheleh Jalali: On the Completeness of Interpolation Algorithms

43:15

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

09:16

Moritz Schubotz: Formal mathematics in zbMATH Open

38:00

Ilka Agricola: CEIC Publication Discussion

49:41

Yutaka Nagashima: Abduction Prover in Isabelle/HOL

59:02

Marco Maggesi: Mechanising Gödel–Löb Provability Logic in HOL Light

50:36

Thaynara Arielly de Lima: "Algebraic Theorems in PVS"

45:03

Alexei Lisitsa: "Gauss Realisability conditions: from error correction to formalization"

48:58

James Davenport: Branch Cuts and Formal Methods?

01:02:17

Mauricio Ayala-Rincón: Formalisation of nominal equations reasoning in PVS*

34:28

Freek Wiedijk: From 100 to 1000+ theorems

33:35

Mario Carneiro: Metamath Zero - Export your Logic

50:31

Michael Kohlhase: Flexiformal Math Libraries

31:18

Sina Hazratpour: HoTT in Lean4

26:58

Thibault Gauthier: Automated Alignments

45:28

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

15:45

Interview with Hélène Esnault on the occasion of Gerd Faltings' 70th birthday

36:58

Florian Rabe: Experiences from Exporting Proof Assistant Libraries

33:05

Luis Berlioz: Text mining the arXiv with LLMs

08:13

Interview with Michael Rapoport on the occasion of Gerd Faltings' 70th birthday

35:10

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

34:22

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

38:29

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

34:43

Fabian Huch: Big Math Libraries in ITPs

28:59

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

41:55

Kensho Tsurusaki: Literate programming in Lean

53:54

Mario Carneiro: Lean4Lean: Formalizing the type theory of Lean

35:20

Rishikesh Vaishnav: Lean4Less - A Term-Patching Framework

56:12

Sandra Alves: Structural Rules and Algebraic Properties of Intersection Types

35:18

Shashank Pathak: GFLean: Autoformalisation for Lean via GF

59:25

Sebastian Ullrich: Profiling Tools in Lean

55:13

Evan Cavallo: Formalizing cubical interpretations of homotopy type theory

56:58

Brigitte Pientka: A Type-Theoretic Framework for Certified Meta-programming

56:15

María Inés de Frutos-Fernández: Local fields in Lean

22:45

Wojciech Nawrocki: Commutative diagrams in Lean (Demo)

13:37

Frederik Schaefer: Annotating and Spotting in Mathematical Corpora (concepts and tools)

49:14

Peter Dybjer: Inductive Definitions, Predicativity, and the Mahlo universe

36:05

Andrea Kolhase: Insights into Search Interfaces for Mathematicians

42:37

Workgroup - Moderation: Mateja Jamnik and Wenda Li

33:42

Wenda Li: Autoformalisation - Bridging the Gap between Informal and Formal Proofs

32:33

Carlos Zapata-Carratala: Hypergraph Rewriting as a Foundation for Diagrammatic Calculus

14:26

Lucy Horowitz: MathGloss and Beyond

01:01:31

Michail Karatarakis: Formalizing Deligne's theorem (Number theory)

37:11

Sander Dahmen and Alain Chavarri Villarello: Computation and formalization

36:31

Valeria de Paiva and Lucy Horowitz: Three prototypes demo (Alignments)

37:12

Silvia de Toffoli: Diagrams and Proofs

38:15

Emily Riehl: Formalizing post-rigorous mathematics

31:22

Adrian De Lon: Natural theorem proving with Naproche-ZF

24:10

Josef Urban: Autoformalization - ten years into the game

39:02

Natarajan Shankar: Cueology of Proof

34:35

Moa Johansson: Neuro-symbolic architectures for assisting autoformalisation & mathematical discovery

36:32

Frederik Schaefer: A Framework for Prototyping Symbolic Natural Language Understanding

48:58

Mateja Jamnik: How can we make trustworthy AI

39:37

Peter Koepke: A Natural Language Formalization of Perfectoid Rings in Naproche

41:36

Milly Maietti and Pietro Sabelli: Peculiarities of the Minimalist Foundation for Formal Mathematics

40:39

Aarne Ranta: Informath: Informalization of Formal Mathematics

24:06

Dennis Müller: Injecting Formal Mathematics into LaTeX

51:37

Valeria de Paiva: Dialectica Categories for all

34:41

Kevin Buzzard: Capturing mathematical equality