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 |
| 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 |
|