Logic and Formalization Seminar at Utrecht University

The Logic and Formalization Seminar is a weekly seminar on topics from logic and formalization. It is run by the logic and formalization group at Utrecht University led by Johan Commelin.

Time and Place

Time: Wednesdays, 13:00 – 14:00 (Fall 2025)
Place: HFG 7.07

Schedule (Spring 2026)

Date	Speaker	Title
22/04/26	Viktor Blåsjö	A historical perspective on formal versus informal mathematics
1/04/26	Jacob Scharmberg	Formalizing Eilenberg-Steenrod homology theories in Lean 4
25/03/26	Johan Commelin	TBA
18/03/26	Christian Merten	TBA
11/03/26	Yu-Lan Dibbits	Formalizing the Consistency of Syntax Theory in Lean: Exploring the usability of mathlib for formal logic
04/03/26	Pim Otte	Lean support in Waterproof
25/02/26	Anne Baanen	Maintaining the Lean Mathematical Library Abstract: Mathlib is one of the fastest growing libraries of formalized mathematics, needing constant maintainer attention to manage this growth. In this talk I will discuss our technical and social solutions for aiming for completeness inside one consistent library, and try to draw some mathematical lessons from some notable (re)design decisions we made along the way.
18/02/26	Benoit Guillemet	TBA
11/02/26	Andrew Yang	Zariski's Main Theorem in Lean Abstract: The latest installment of the saga: How much AG can we do without cohomology?
04/02/26	Jelle Wemmenhove	Towards a practical implementation of limits in Lean
28/01/26	Fernando Chu	Directed Type Theory, with a twist

Schedule (Fall 2025)

Date	Speaker	Title
17/12/25	Jovan Gerbscheid	New tools for theorem proving in Lean Abstract: I will present some tactics and tools that I made for Mathlib. I will explain how they work and show them in action with a live demonstration. These include: 1. A library search tool for finding theorems based on an expression in the tactic state. 2. The generalized rewriting tactic for rewriting with relations other than equalities. 3. The to_dual attribute for automatically generating dual versions of theorems.
10/12/25	Vincent Kuhlmann	Proof transfer in Lean: my experiences implementing Trocq
03/12/25	Benoît Guillemet	TBA
26/11/25	Raphael Douglas Giles(?)	TBA
12/11/25	Pim Otte	Discussion session inspired by the Mechanization and Mathematical Research Workshop (continued)
5/11/25	Edward van de Meent	Topoi
29/10/25	Pim Otte	Discussion session inspired by the Mechanization and Mathematical Research Workshop (ends at 14:45)
22/10/25	Jelle Wemmenhove	Proof assistants in math education - my experience
15/10/25	Jiedong Jiang	The FATE of AI Formal Reasoning: Challenging LLMs with Formal Frontier Algebra
08/10/25	Ioli Tente	Model Checking on graphs and the Least Fixed Point Logic
01/10/25	Yu Lan	Formalizing Syntax Theory and Derivations
24/09/25	Christian Merten	The spec of a good database library in Lean
17/09/25	Fernando Chu	A brief introduction to semantics of dependent type theory

Schedule (Spring 2025)

Date	Speaker	Title
11/06/25	Alex van Tilburg	Waterproof for "Introduction to proofs"
04/06/25	Pim Otte	My past open source life and my favourite algorithm
28/05/25	Quinn van der Velden	Construction of classifying categories as term models
21/05/25	Christian Merten	Formalising the étale fundamental group
14/05/25	Johan Commelin	Liquid Tensor Experiment
07/05/25	No seminar
30/04/25	Johan Commelin	Condensed type theory
23/04/25	Christian Merten	autograde - automatically grading Lean submissions in Lean
16/04/25	Vincent Kuhlmann	Trocq in Lean
09/04/25	Sam Lindauer	Formalizing differential forms
02/04/25	Fernando Chu	Observability Type Theory
26/03/25	Raphael Douglas Giles	TBA
19/03/25	~~Vincent Kuhlmann~~	~~Trocq in Lean~~ (Cancelled)
12/03/25	Quinn van der Velden	Partial categorical logic
26/02/25	No seminar
19/02/25	No seminar
12/02/25	Vincent Kuhlmann	Trocq
05/02/25	Planning session