May
June
Mon 3, 15:00 
Chris Lam: Adventures in CorrectbyConstruction Proof Engineering 
Tue 4, 15:00 
Harshit Motwani: Formal Verification and Synthesis of Polynomial Programs using AlgebroGeometry 
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 

Fri 14, 15:00 
James Davenport: Proving an execution of an algorithm correct
Link to paper: https://doi.org/10.1007/9783031427534_17
James Davenport: Proving an execution of an algorithm correct
Nicolas Thiéry (Université ParisSaclay): 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)
(Recording has not been edited, yet)
Video not found
Andrea Kohlhase: Eye Tracking for Math
Reed Mullanix: Cubical Type Theory for the LowDimensional Mathematician
(Pending permission to publish the recording)
Video not found
Emily Riehl (Johns Hopkins University): Formalizing ∞category theory in the Rzk proof assistant
Link to repository: https://emilyriehl.github.io/yoneda/CPP2024/
Link to slides: https://emilyriehl.github.io/files/colloquiumyonedainrzk.pdf
Emily Riehl: Formalizing ∞category theory in the Rzk proof assistant
Tom de Jong (University of Nottingham): Formalization in HoTT: equivalences, 3for2 and definitional equality
Tom de Jong: Formalization in HoTT: equivalences, 3for2 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, UrbanaChampaign): Adventures in CorrectbyConstruction Proof Engineering
Link to paper: https://doi.org/10.1145/3586052
(Pending permission to publish the recording)
Video not found
Harshit Motwani (Hong Kong University of Science and Technology): Formal Verification and Synthesis of Polynomial Programs using AlgebroGeometry
Link to paper: https://doi.org/10.1145/3586052
(No recording available)
Juan Meleiro (Universidade de São Paulo): Theoryoriented mathematics
Juan Meleiro: Theoryoriented 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, ISTICNR): Doctrines for Formal Mathematics
Davide Trotta: Doctrines for Formal Mathematics
Sina Hazratpour (Johns Hopkins): Linear Algebra Game in Lean
Link to repository: https://github.com/hhuadam/Robo/tree/main
Sina Hazratpour: Linear Algebra Game in Lean