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

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.

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

Fingerprint

Number theory
Polynomials

Keywords

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

Cite this

Lewis, R. Y. (2019). A formal proof of Hensel's lemma over the p-adic integers. In A. Mahboubi (Ed.), CPP 2019 - Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2019 (pp. 15-26). Association for Computing Machinery, Inc. https://doi.org/10.1145/3293880.3294089
Lewis, Robert Y. / A formal proof of Hensel's lemma over the p-adic integers. CPP 2019 - Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2019. editor / Assia Mahboubi. Association for Computing Machinery, Inc, 2019. pp. 15-26
@inproceedings{8dc9c27c908d4a839136cb1f87a8ca02,
title = "A formal proof of Hensel's lemma over the p-adic integers",
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.",
keywords = "formal proof, Hensel's lemma, Lean, p-adic",
author = "Lewis, {Robert Y.}",
year = "2019",
month = "1",
day = "14",
doi = "10.1145/3293880.3294089",
language = "English",
pages = "15--26",
editor = "Assia Mahboubi",
booktitle = "CPP 2019 - Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2019",
publisher = "Association for Computing Machinery, Inc",

}

Lewis, RY 2019, A formal proof of Hensel's lemma over the p-adic integers. in A Mahboubi (ed.), CPP 2019 - Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2019. Association for Computing Machinery, Inc, pp. 15-26, 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, 14/01/19. https://doi.org/10.1145/3293880.3294089

A formal proof of Hensel's lemma over the p-adic integers. / Lewis, Robert Y.

CPP 2019 - Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2019. ed. / Assia Mahboubi. Association for Computing Machinery, Inc, 2019. p. 15-26.

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

TY - GEN

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

AU - Lewis, Robert Y.

PY - 2019/1/14

Y1 - 2019/1/14

N2 - 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.

AB - 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.

KW - formal proof

KW - Hensel's lemma

KW - Lean

KW - p-adic

UR - http://www.scopus.com/inward/record.url?scp=85061177132&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85061177132&partnerID=8YFLogxK

U2 - 10.1145/3293880.3294089

DO - 10.1145/3293880.3294089

M3 - Conference contribution

SP - 15

EP - 26

BT - CPP 2019 - Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2019

A2 - Mahboubi, Assia

PB - Association for Computing Machinery, Inc

ER -

Lewis RY. A formal proof of Hensel's lemma over the p-adic integers. In Mahboubi A, editor, CPP 2019 - Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2019. Association for Computing Machinery, Inc. 2019. p. 15-26 https://doi.org/10.1145/3293880.3294089