New Frontiers of Formal Proof Revolution

March 06, 2025

IPM Mathematics Seminars, IPM Institute For Research In Fundamental Sciences, Tehran

HoTTLean : Formalizing the Meta-Theory of HoTT in Lean

February 19, 2025

Logic Seminars at Stockholm Mathematics Centre, Department of Mathematics, University of Stockholm, Albano house 1, floor 3, Room U (Kovalevsky)

Linear Algebra Game in Lean4

June 19, 2024

Trimester in Prospects of Formal Mathematics, Hausdorff Research Institute in Mathematics (HIM), Bonn

A game to learn linear algebra in Lean4 at Heinrich Heine University, Düsseldorf

Formalization of Polynomial Functors in Lean 4

June 11, 2024

Trimester in Prospects of Formal Mathematics, Hausdorff Research Institute in Mathematics (HIM), Bonn

Fibred and Displayed Categories in Lean 4

April 16, 2024

Dutch Formal Methods Day 2024, Univeristy of Utrecht

A modular approach to fibred in Lean 4

Teaching Introduction To Proofs With Lean

January 11, 2023

Seminar Talk, TU Delft Programming Language Group

In Fall 2022, I taught an undergraduate course in the Mathematics Department at Johns Hopkins University entitled “Introduction to Proofs” entirely with the Lean Proof Assistant. In this talk, I will report on this teaching experiment.

A 2-Categorical Proof of Frobenius for Fibrations Defined From a Generic Point

June 28, 2022

MURI Meeting 2022, Carnegie Mellon University, Pittsburgh, USA

An earlier version of this talk was given at JHU Category Theory SeminarSeminars.

Kripke Joyal Semantics For Homotopy Type Theory

April 09, 2022

Association for Symbolic Logic, 2022 Annual Meeting, Cornell University, Ithaca, USA

A talk based on the paper “Kripke-Joyal forcing for type theory and uniform fibrations” with Steve Awodey and Nicola Gambino.

The Roots of Intuitionistic and Constructive Mathematics

January 17, 2021

Kripke Joyal Semantics For Dependent Type Theory

December 11, 2020

HoTT Seminar, Pittsburgh HoTT Seminar

The result here was earlier presented at the Yorkshire and Midlands Category Theory Seminars (YaMCATS) and Ghent–Leeds Virtual Logic Seminar and also at CATS seminars at ILLC, UvA, Amsterdam.

Bicategorical Comprehension Construction And Fibration Of Toposes

June 20, 2019

Conference talk, TACL 2019, Laboratoire Mathématiques J.A. Dieudonné, Université Côte d’Azur, Parc Valrose

Toposes In Como

June 29, 2018

Conference talk, Toposes in Como, Chiostro di Sant’Abbondio, Università degli Studi dell’Insubria

• Recoring of the talk on YouTube

Fibrations Of Bicategories And Fibrations Of Toposes

March 21, 2018

Conference talk, YaMCATS, School of Mathematics, University of Sheffield

Fibrations of Toposes and Etale Maps

September 16, 2017

Conference talk, PSSL 101, School of Mathematics, University of Leeds