May
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 |
|
| Thu 6, 15:00 |
Milly Maietti and Pietro Sabelli: Peculiarities of the Minimalist Foundation for Formal Mathematics |
| Fri 7, 15:00 |
|
| Mon 10, 15:00 |
Sina Hazratpour: Report on Polynomial Functors Formalization |
| Tue 11, 15:00 |
|
| Wed 12, 15:00 |
|
| Thu 13, 15:00 |
|
| Fri 14, 15:00 |
|
| Mon 24, 15:00 | |
| Tue 25, 15:00 |
Mirna Džamonja: Calculating ordinal invariants - can you do better than a human? |
| Wed 26, 15:00 |
|
| 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 | |
| Tue 2, 15:00 |
|
| Wed 3, 15:00 |
Michael Kohlhase: Aspects of Mathematical Knowledge - The Tetrapod Model |
| Thu 4, 15:00 |
|
| Fri 5, 15:00 |
Paul Andre Mellies: Fierce Discussion about ML and Proof 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
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
Michail Karatarakis: Formalizing Deligne's theorem (Number theory)
(Pending permission to publish the recording)
Video not found
Andrea Kohlhase: Eye Tracking for Math
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
Tom de Jong (University of Nottingham): Formalization in HoTT: equivalences, 3-for-2 and definitional equality
Tom de Jong: Formalization in HoTT: equivalences, 3-for-2 and definitional equality
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
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
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
Cipriano Cioffo (Università degli Studi di Padova): A categorical account of the setoid model
Cipriano Cioffo: A categorical account of the setoid model
Sina Hazratpour (Johns Hopkins): Report on Polynomial Functors Formalization
Link to repository: https://github.com/sinhp/Poly/
Sina Hazratpour: Report on Polynomial Functors Formalization
Valeria de Paiva (Topos Institute): AI tools for Better Math
Valeria de Paiva: AI tools for Better Math
Davide Trotta (National Research Council, ISTI-CNR): Doctrines for Formal Mathematics
Davide Trotta: Doctrines for Formal Mathematics
Dagur Asgeirsson (University of Copenhagen): Condensed mathematics in Mathlib
Dagur Asgeirsson: Condensed mathematics in Mathlib
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
Mario Carneiro (Carnegie Mellon University): Impromptu chat about HB in Lean
Mario Carneiro: Impromptu chat about HB in Lean
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 ?
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
Valeria de Paiva (Topos Institute): Dialectica Categories for all
Valeria de Paiva: Dialectica Categories for all
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
Michael Kohlhase (FAU Erlangen-Nürnberg): Aspects of Mathematical Knowledge - The Tetrapod Model
Michael Kohlhase: Aspects of Mathematical Knowledge - The Tetrapod Model
Sebastian Ullrich (Lean FRO): Profiling Tools in Lean
Sebastian Ullrich: Profiling Tools in Lean
Paul-André Melliès (CNRS, Universite Paris Cite, INRIA): Fierce Discussion about ML and Proof Theory
(No recording available)