Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal

The field of p-adic numbers Qp and the ring of p-adic integers Zp are essential constructions of modern number theory. Hensel’s lemma, described by Gouvêa as the “most important algebraic property of the p-adic numbers”, shows the existence of roots of polynomials over Zp provided an initial seed point. The theorem can be proved for the p-adics with significantly weaker hypotheses than for general rings. We construct Qp and Zp in the Lean proof assistant, with various associated algebraic properties, and formally prove a strong form of Hensel’s lemma. The proof lies at the intersection of algebraic and analytic reasoning and demonstrates how the Lean mathematical library handles such a heterogeneous topic.

Mon 14 Jan

Displayed time zone: Belfast change

16:00 - 17:30
Research Papers: Formalization of Mathematics and Computer AlgebraCPP at Sala XII
Chair(s): Georges Gonthier Inria
16:00
30m
Research paper
A Formal Proof of Hensel's Lemma over the p-adic Integers
CPP
Robert Y. Lewis Vrije Universiteit Amsterdam
DOI
16:30
30m
Research paper
Counting Polynomial Roots in Isabelle/HOL: A formal Proof of the Budan-Fourier Theorem
CPP
Wenda Li University of Cambridge, Lawrence Paulson University of Cambridge
DOI
17:00
30m
Research paper
Smooth Manifolds and Types to Sets for Linear Algebra in Isabelle/HOL
CPP
DOI