Seminar Series

May

Tue 21, 15:00	James Davenport: Proving an execution of an algorithm correct¹
Wed 22, 15:00	Nicolas Thiéry: Categories, axioms, constructions in SageMath: Modeling mathematics for fun and profit²
Thu 23, 14:00	Michail Karatarakis: Formalizing Deligne's theorem (Number theory)³
Fri 24, 15:00	Andrea Kohlhase: Eye Tracking for Math⁴
Mon 27, 15:00	Reed Mullanix: Cubical Type Theory for the Low-Dimensional Mathematician⁵
Tue 28, 15:00	Emily Riehl: Formalizing ∞-category theory in the Rzk proof assistant⁶
Wed 29, 15:00	Tom de Jong: Formalization in HoTT: equivalences, 3-for-2 and definitional equality⁷
Fri 31, 15:00	Claudio Sacerdoti Coen: Indexing and Retrieval in a heterogeneous Formal Library⁸

June

Mon 3, 15:00	Chris Lam: Adventures in Correct-by-Construction Proof Engineering⁹
Tue 4, 15:00	Harshit Motwani: Formal Verification and Synthesis of Polynomial Programs using Algebro-Geometry¹⁰
Wed 5, 15:00	Juan Meleiro: Theory-oriented mathematics¹¹
Thu 6, 15:00	Milly Maietti and Pietro Sabelli: Peculiarities of the Minimalist Foundation for Formal Mathematics¹²
Fri 7, 15:00	Cipriano Cioffo: A categorical account of the setoid model¹³
Mon 10, 15:00	Sina Hazratpour: Report on Polynomial Functors Formalization¹⁴
Tue 11, 15:00	Valeria de Paiva: AI tools for Better Math¹⁵
Wed 12, 15:00	Davide Trotta: Doctrines for Formal Mathematics¹⁶
Thu 13, 15:00	Dagur Asgeirsson: Condensed mathematics in Mathlib¹⁷
Fri 14, 15:00	Sina Hazratpour: Linear Algebra Game in Lean¹⁸
Mon 24, 15:00	Mario Carneiro: Impromptu chat about HB in Lean¹⁹
Tue 25, 15:00	Mirna Džamonja: Calculating ordinal invariants - can you do better than a human?²⁰
Wed 26, 15:00	Jeremy Avigad: A dry run²¹
Thu 27, 15:00	Thomas Ammer: Formalising and Verifying Algorithms for the Minimum Cost Flow Problem²²
Fri 28, 15:00	Maximilian Doré: Automating Reasoning in Cubical Type Theory²³

July

Mon 1, 15:00	Valeria de Paiva: Dialectica Categories for all²⁴
Tue 2, 15:00	Josef Urban: The Proofgold blockchain²⁵
Wed 3, 15:00	Michael Kohlhase: Aspects of Mathematical Knowledge - The Tetrapod Model²⁶
Thu 4, 15:00	Sebastian Ullrich: Profiling Tools in Lean²⁷
Fri 5, 15:00	Paul Andre Mellies: Fierce Discussion about ML and Proof Theory²⁸
Mon 15, 15:00	Peter Dybjer: Inductive Definitions, Predicativity, and the Mahlo universe²⁹
Tue 16, 15:00	Sina Hazratpour: Dependent Equalities in Lean4³⁰
Thu 18, 15:00	Evan Cavallo: Formalizing cubical interpretations of homotopy type theory³¹
Fri 19, 15:00	Gisele D. Secco: From Computers to Diagrams and Back: The Four-Color Theorem and the Rise of a New Mathemartical Culture³²
Mon 22, 15:00	Shashank Pathak: GFLean: Autoformalisation for Lean via GF³³
Tue 23, 15:00	Rishikesh Vaishnav: Lean4Less - A Term-Patching Framework for Eliminating Defitional Equalities in Lean³⁴
Wed 24, 15:00	Mario Carneiro: Lean4Lean - Formalizing the metatheory of Lean³⁵
Thu 25, 15:00	Kensho Tsurusaki: Literate programming in Lean³⁶

August

Mon 5, 15:00	Mauricio Ayala-Rincón: Formalisation of nominal equations reasoning in PVS³⁷
Tue 6, 15:00	James Davenport: Branch Cuts and Formal Methods?³⁸
Wed 7, 15:00	James Mckinna: Reflections on a career with/in type theory for formalised computer science/math³⁹
Thu 8, 15:00	Marco Maggesi: Mechanising Gödel–Löb Provability Logic in HOL Light⁴⁰
Fri 9, 15:00	Thaynara Arielly de Lima: Algebraic Theorems in PVS⁴¹
Mon 12, 15:00	Alexei Lisitsa: Gauss Realisability conditions - from error correction to formalization⁴²
Tue 13, 15:00	Yutaka Nagashima: Abduction Prover in Isabelle/HOL⁴³
Wed 14, 15:00	Raheleh Jalali: On the Completeness of Interpolation Algorithms⁴⁴
Wed 14, 15:30	Hannah Leung: Formally Verifying Functional Correctness of a Path Oblivious RAM algorithm⁴⁵
Thu 15, 15:00	Marco Caminati: Challenges in formalising recent results in formal language theory⁴⁶

James Davenport: Proving an execution of an algorithm correct

Link to paper: https://doi.org/10.1007/978-3-031-42753-4_17⁴⁷

James Davenport: Proving an execution of an algorithm correct

Bild © Hausdorff Center for Mathematics / YouTube

Nicolas Thiéry (Université Paris-Saclay): Categories, axioms, constructions in SageMath: Modeling mathematics for fun and profit

Link to slides: https://zenodo.org/records/12079015⁴⁸

Nicolas Thiéry: Categories, axioms, constructions in SageMath: Modeling mathematics for fun and profit

Bild © Hausdorff Center for Mathematics / YouTube

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

Bild © Hausdorff Center for Mathematics / YouTube

Andrea Kohlhase: Eye Tracking for Math

Link to slides⁴⁹

Andrea Kohlhase: Eye Tracking for Math

Bild © Hausdorff Center for Mathematics / YouTube

Reed Mullanix: Cubical Type Theory for the Low-Dimensional Mathematician

(No recording available)

Emily Riehl (Johns Hopkins University): Formalizing ∞-category theory in the Rzk proof assistant

Link to repository: https://emilyriehl.github.io/yoneda/CPP-2024/⁵⁰

Link to slides: https://emilyriehl.github.io/files/colloquium-yoneda-in-rzk.pdf⁵¹

Emily Riehl: Formalizing ∞-category theory in the Rzk proof assistant

Bild © Hausdorff Center for Mathematics / YouTube

Tom de Jong (University of Nottingham): Formalization in HoTT: equivalences, 3-for-2 and definitional equality

https://fplunchnott.wordpress.com/2023/12/08/a-practical-technique-for-proving-that-a-map-is-an-equivalence/⁵²

Tom de Jong: Formalization in HoTT: equivalences, 3-for-2 and definitional equality

Bild © Hausdorff Center for Mathematics / YouTube

Claudio Sacerdoti Coen (Alma Mater Studiorum - Università di Bologna): Indexing and Retrieval in a heterogeneous Formal Library

Claudio Sacerdoti Coen: Indexing and Retrieval in a heterogeneous Formal Library

Bild © Hausdorff Center for Mathematics / YouTube

Chris Lam (University of Illinois, Urbana-Champaign): Adventures in Correct-by-Construction Proof Engineering

Link to paper: https://doi.org/10.1145/3586052⁵³

(No recording available)

Harshit Motwani (Hong Kong University of Science and Technology): Formal Verification and Synthesis of Polynomial Programs using Algebro-Geometry

Link to paper: https://doi.org/10.1145/3586052⁵³

(No recording available)

Juan Meleiro (Universidade de São Paulo): Theory-oriented mathematics

Juan Meleiro: Theory-oriented mathematics

Bild © Hausdorff Center for Mathematics / YouTube

Milly Maietti (University of Padova) and Pietro Sabelli (University of Padua): Peculiarities of the Minimalist Foundation for Formal Mathematics

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

Bild © Hausdorff Center for Mathematics / YouTube

Cipriano Cioffo (Università degli Studi di Padova): A categorical account of the setoid model

Cipriano Cioffo: A categorical account of the setoid model

Bild © Hausdorff Center for Mathematics / YouTube

Sina Hazratpour (Johns Hopkins): Report on Polynomial Functors Formalization

Link to repository: https://github.com/sinhp/Poly/⁵⁴

Sina Hazratpour: Report on Polynomial Functors Formalization

Bild © Hausdorff Center for Mathematics / YouTube

Valeria de Paiva (Topos Institute): AI tools for Better Math

Valeria de Paiva: AI tools for Better Math

Bild © Hausdorff Center for Mathematics / YouTube

Davide Trotta (National Research Council, ISTI-CNR): Doctrines for Formal Mathematics

Link to slides⁵⁵

Davide Trotta: Doctrines for Formal Mathematics

Bild © Hausdorff Center for Mathematics / YouTube

Dagur Asgeirsson (University of Copenhagen): Condensed mathematics in Mathlib

Dagur Asgeirsson: Condensed mathematics in Mathlib

Bild © Hausdorff Center for Mathematics / YouTube

Sina Hazratpour (Johns Hopkins): Linear Algebra Game in Lean

Link to repository: https://github.com/hhu-adam/Robo/tree/main⁵⁶

Sina Hazratpour: Linear Algebra Game in Lean

Bild © Hausdorff Center for Mathematics / YouTube

Mario Carneiro (Carnegie Mellon University): Impromptu chat about HB in Lean

Mario Carneiro: Impromptu chat about HB in Lean

Bild © Hausdorff Center for Mathematics / YouTube

Mirna Džamonja (IRIF (CNRS et Université Paris Cité) ): Calculating ordinal invariants - can you do better than a human ?

Mirna Džamonja: Calculating ordinal invariants - can you do better than a human ?

Bild © Hausdorff Center for Mathematics / YouTube

Jeremy Avigad (Carnegie Mellon University): A dry run

(No recording available)

Thomas Ammer (King's College London): Formalising and Verifying Algorithms for the Minimum Cost Flow Problem

(No recording available)

Maximilian Doré (Oxford University): Automating Reasoning in Cubical Type Theory

Maximilian Doré : Automating Reasoning in Cubical Type Theory

Bild © Hausdorff Center for Mathematics / YouTube

Valeria de Paiva (Topos Institute): Dialectica Categories for all

Valeria de Paiva: Dialectica Categories for all

Bild © Hausdorff Center for Mathematics / YouTube

Josef Urban (CIIRC - CTU): The Proofgold blockchain

Link to paper: https://doi.org/10.4230/OASIcs.FMBC.2022.4⁵⁷

See also: https://formalweb3.uibk.ac.at/pgbce/⁵⁸

Josef Urban: The Proofgold blockchain

Bild © Hausdorff Center for Mathematics / YouTube

Michael Kohlhase (FAU Erlangen-Nürnberg): Aspects of Mathematical Knowledge - The Tetrapod Model

Michael Kohlhase: Aspects of Mathematical Knowledge - The Tetrapod Model

Bild © Hausdorff Center for Mathematics / YouTube

Sebastian Ullrich (Lean FRO): Profiling Tools in Lean

Sebastian Ullrich: Profiling Tools in Lean

Bild © Hausdorff Center for Mathematics / YouTube

Paul-André Melliès (CNRS, Universite Paris Cite, INRIA): Fierce Discussion about ML and Proof Theory

(No recording available)

Peter Dybjer (Chalmers University of Technology): Inductive Definitions, Predicativity, and the Mahlo universe

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

Bild © Hausdorff Center for Mathematics / YouTube

Sina Hazratpour (Johns Hopkins University): Dependent Equalities in Lean4

(No recording available)

Link to repository: https://github.com/sinhp/LeanFibredCategories⁵⁹

Evan Cavallo (Göteborgs universitet): Formalizing cubical interpretations of homotopy type theory

See https://arxiv.org/abs/2406.18497 ⁶⁰and https://ecavallo.net/equivariant-cartesian/⁶¹

Evan Cavallo: Formalizing cubical interpretations of homotopy type theory

Bild © Hausdorff Center for Mathematics / YouTube

Gisele D. Secco (California State University San Bernardino): From Computers to Diagrams and Back: The Four-Color Theorem and the Rise of a New Mathemartical Culture

(No recording available)

Shashank Pathak (The University of Manchester): GFLean - Autoformalisation for Lean via GF

Link to paper: https://arxiv.org/abs/2404.01234⁶²

Shashank Pathak: GFLean: Autoformalisation for Lean via GF

Rishikesh Vaishnav (École normale supérieure Paris-Saclay): Lean4Less - A Term-Patching Framework for Eliminating Defitional Equalities in Lean (Work in Progress)

Link to paper: https://lfmtp.github.io/lfmtp-page/workshops/2024/wip_1_vaishnav.pdf⁶³

Rishikesh Vaishnav: Lean4Less: A Term-Patching Framework for Eliminating Defitional Equalities in Lean

Mario Carneiro (Carnegie Mellon University): Lean4Lean - Formalizing the metatheory of Lean

Link to slides⁶⁴

Mario Carneiro: Lean4Lean: Formalizing the type theory of Lean

Kensho Tsurusaki (The University of Tokyo): Literate programming in Lean

I'll talk about implementing a system for "literate programming" in Lean.

Link to slides: https://drive.google.com/file/d/1GzrJ6liwSMrHTYZCLCyqo42FVCMa4v2X/view?usp=sharing⁶⁵

Kensho Tsurusaki: Literate programming in Lean

Mauricio Ayala-Rincón (Universidade de Brasília): Formalisation of nominal equations reasoning in PVS*

Nominal anti-unification (the library nasa/ pvslib/ nominal)

* Research supported by Brazilian agencies CAPES, CNPq, and FAPDF

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

James Davenport (University of Bath): Branch Cuts and Formal Methods?

Link to updated slides: https://people.bath.ac.uk/masjhd/Slides/JHDatHIMBranchCuts.pdf⁶⁶

James Davenport: Branch Cuts and Formal Methods?

James Mckinna (Heriot-Watt University): Reflections on a career with/in type theory for formalised computer science/math

(No recording available)

Marco Maggesi (Università di Firenze): Mechanising Gödel–Löb Provability Logic in HOL Light

Link to paper: https://link.springer.com/article/10.1007/s10817-023-09677-z⁶⁷

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

Thaynara Arielly de Lima (Universidade Federal de Goiás): Algebraic Theorems in PVS

Thaynara Arielly de Lima: Algebraic Theorems in PVS

Alexei Lisitsa (University of Liverpool): Gauss Realisability conditions - from error correction to formalization

Links to further resources:

https://arxiv.org/pdf/2103.02102⁶⁸
https://arxiv.org/abs/2108.02873⁶⁹
https://www.worldscientific.com/toc/jktr/32/10⁷⁰

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

Yutaka Nagashima (Independent): Abduction Prover in Isabelle/HOL

Raheleh Jalali (Institute of Computer Science, Czech Academy of Sciences): On the Completeness of Interpolation Algorithms

Link to publications:

Raheleh Jalali: On the Completeness of Interpolation Algorithms

Hannah Leung (University of Illinois Urbana-Champaign): Formally Verifying Functional Correctness of a Path Oblivious RAM algorithm

(No recording available)

Marco Caminati (Lancaster University Leipzig): Challenges in formalising recent results in formal language theory

In a recent paper (https://arxiv.org/abs/2405.09396⁷³), I introduced a new proof of a recent result linking formal language theory and computational group theory, one goal being to make its formalisation more feasible. I will discuss the state of this.

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

Back up ⁷⁴