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, 14:00 – 15:00 (Fall 2025)
- Place
- HFG 7.07
Schedule (Fall 2025)
| Date | Speaker | Title |
|---|---|---|
| 25/02/26 | Anne Baanen | TBA |
| 18/02/26 | Benoit Guillemet | TBA |
| 11/02/26 | Andrew Yang |
Zariski's Main Theorem in LeanAbstract: 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 |
| 17/12/25 | Jovan Gerbscheid |
New tools for theorem proving in LeanAbstract: 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 | ||
| 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 |