Valued rings and fields are ubiquitous in mathematics. Consider, for example, Laurent series in analysis, the p-adic numbers in number theory or discrete valuation rings in algebraic geometry. The lens of model theory provides powerful tools to study them. One key application consists of transfer principles in the spirit of the Ax-Kochen-Ershov theorem, which implies in particular a transfer principle for first-order statements between ℚ_p and 𝔽_p((t)) (for sufficiently large p). A notable extension of this idea is given by the theory of motivic integration, which achieves a similar transfer statement on the level of integrals.

With the recent rise of formalization as a mathematical discipline, one might dream of formalizing these theorems. Yet, most of them cannot yet be stated in proof assistants. We are working on bridging that gap by developing the requisite model theory in Lean 4. This is a joint project with D. Haskell, A. Crighton and J. Nicholson, situated at the Fields Institute and McMaster University.