Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Sun 17 Jan 2021 18:45 - 19:00 at CPP - Formalized Mathematics Chair(s): Amin Timany

The ring of Witt vectors $\mathbb{W} R$ over a base ring $R$ is an important tool in algebraic number theory and lies at the foundations of modern $p$-adic Hodge theory. $\mathbb{W} R$ has the interesting property that it constructs a ring of characteristic $0$ out of a ring of characteristic $p > 1$, and it can be used more specifically to construct from a finite field containing $\mathbb{Z}/p\mathbb{Z}$ the corresponding unramified field extension of the $p$-adic numbers~$\mathbb{Q}_p$ (which is unique up to isomorphism).

We formalize the notion of a Witt vector in the Lean proof assistant, along with the corresponding ring operations and other algebraic structure. We prove in Lean that, for prime $p$, the ring of Witt vectors over $\mathbb{Z}/p\mathbb{Z}$ is isomorphic to the ring of $p$-adic integers $\mathbb{Z}_p$. In the process we develop idioms to cleanly handle calculations of identities between operations on the ring of Witt vectors. These calculations are intractible with a naive approach, and require a proof technique that is usually skimmed over in the informal literature.

Sun 17 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

18:45 - 19:30
Formalized MathematicsCPP at CPP
Chair(s): Amin Timany Aarhus University

Streamed session: https://youtu.be/U_ZT9hfDAUQ?t=2768

18:45
15m
Talk
Formalizing the Ring of Witt VectorsDistinguished Paper Award
CPP
Johan Commelin Universität Freiburg, Robert Y. Lewis Vrije Universiteit Amsterdam
Pre-print Media Attached
19:00
15m
Talk
Formal Verification of Semi-algebraic Sets and Real Analytic Functions
CPP
J Tanner Slagel NASA Langley Research Center, Lauren White Kansas State University, Aaron Dutle NASA Langley Research Center
Pre-print Media Attached
19:15
15m
Talk
On the Formalisation of Kolmogorov Complexity
CPP
Elliot Catt ANU, Michael Norrish Data61, CSIRO & ANU
Pre-print Media Attached