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

Robert Y. Lewis*

*Corresponding author for this work

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

Abstract

The field of p-adic numbers p and the ring of p-adic integers p are essential constructions of modern number theory. Hensels lemma, described by Gouva as the most important algebraic property of the p-adic numbers, shows the existence of roots of polynomials over 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 p and p in the Lean proof assistant, with various associated algebraic properties, and formally prove a strong form of Hensels lemma. The proof lies at the intersection of algebraic and analytic reasoning and demonstrates how the Lean mathematical library handles such a heterogeneous topic.

Original languageEnglish
Title of host publicationCPP 2019 - Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2019
EditorsAssia Mahboubi
PublisherAssociation for Computing Machinery, Inc
Pages15-26
Number of pages12
ISBN (Electronic)9781450362221
DOIs
Publication statusPublished - 14 Jan 2019
Event8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019 - Cascais, Portugal
Duration: 14 Jan 201915 Jan 2019

Conference

Conference8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019
CountryPortugal
CityCascais
Period14/01/1915/01/19

Keywords

  • formal proof
  • Hensel's lemma
  • Lean
  • p-adic

Fingerprint Dive into the research topics of 'A formal proof of Hensel's lemma over the p-adic integers'. Together they form a unique fingerprint.

Cite this