A formal proof of Hensel's lemma over the p-adic integers

Abstract

The field of \(p\)-adic numbers \(\mathbb{Q}_p\) and the ring of \(p\)-adic integers \(\mathbb{Z}_p\) are essential constructions of modern number theory. Hensel's lemma, described by Gouv\^ea as the "most important algebraic property of the \(p\)-adic numbers," shows the existence of roots of polynomials over \(\mathbb{Z}_p\) provided an initial seed point. The theorem can be proved for the \(p\)-adics with significantly weaker hypotheses than for general rings. We construct \(\mathbb{Q}_p\) and \(\mathbb{Z}_p\) 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.