Formalizing the Model Theory of Valued Fields

In recent years, formal proof verification has become an important mathematical topic in its own right. Modern interactive theorem provers such as Lean 4 provide powerful automation tools that bring us closer to a new reality where new mathematical discoveries also come with a formal certificate of soundness. However, to make this into a reality, more foundational results need to be formalized.

Large steps have already been taken by Lean's Mathlib library, containing essentially all of undergraduate mathematics. Yet, for most fields of mathematics, there is still a significant gap between what exists in the library and research-level mathematics.

We are leading an effort to bridge this gap for the model theory of valued fields. In particular, we will formalize relative quantifier elimination and the Ax-Kochen/Ersov principles. These are important tools in current research, underpinning e.g. frameworks for motivic integration, but they also have immediate consequences of interest to algebraic geometers and number theorists. While working towards this concrete goal, many supporting results with wide applicability will be developed, including quantifier elimination tests, and more fundamentally an extension of Lean's model theory library to the many-sorted setting.

You can check in on our progress at

https://github.com/Mathias-Stout/Many-sorted-model-theory

This repository is maintained by Aaron Crighton, John Nicholson and Mathias Stout.
----
Points of contact:

Deirdre Haskell
Aaron Crighton
Greg Cousins
John Nicholson
Mathias Stout