Date/Time
Date(s) - 03/11/2025
2:30 pm - 4:30 pm

Location: Hamilton Hall, Room 410

Speaker: Mathias Stout (McMaster University)

Title: Model theory in Lean

Abstract:
In this informal talk, I will discuss progress on an ongoing effort to formalize the foundations of the model theory of valued fields in Lean 4, from a mathematician’s point of view. More accurately, I will discuss the formalization of the necessary foundations of multisorted logic to attempt such a project in a principled manner.

In the course of this talk, I will attempt to answer the following questions:

* Why formalize mathematics?

* Can anyone formalize mathematics?

* Why is dependent type theory great?

* What is ‘dependent type hell’?

Coffee and snacks will appear around 2:30 and the talk will start at 3:30pm. Afterwards this group will head to the Phoenix for a drink.