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.
This based on work in collaboration with A. Crighton, G. Cousins, D. Haskell and J. Nicholson
