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

TL;DR

This paper constructs the $p$-adic numbers and integers in Lean and provides a formal proof of a strong form of Hensel's lemma, bridging algebraic and analytic reasoning.

Contribution

It offers the first formal proof of Hensel's lemma over $\

Findings

Constructed $\\mathbb{Q}_p$ and $\\mathbb{Z}_p$ in Lean

Proved a strong form of Hensel's lemma formally

Demonstrated handling of algebraic and analytic reasoning in Lean

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.