Date/Time Date(s) - 09/02/202612:30 pm - 1:30 pm
Speaker: Mathias Stout (McMaster University)
Location: Hamilton Hall, Room 410
Title: Towards model theory of valued fields in Lean
Abstract: I will report on an ongoing project on building a formalized library of the foundational model theory of valued fields in Lean. It turns out that even formalizing the requisite many-sorted model theory is already an interesting and sometimes subtle challenge. I will indicate these challenges and sketch the way forward, without assuming any background in Lean.