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 language | English |
|---|---|
| Title of host publication | CPP 2019 - Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2019 |
| Editors | Assia Mahboubi |
| Publisher | Association for Computing Machinery, Inc |
| Pages | 15-26 |
| Number of pages | 12 |
| ISBN (Electronic) | 9781450362221 |
| DOIs | |
| Publication status | Published - 14 Jan 2019 |
| Event | 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019 - Cascais, Portugal Duration: 14 Jan 2019 → 15 Jan 2019 |
Conference
| Conference | 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019 |
|---|---|
| Country | Portugal |
| City | Cascais |
| Period | 14/01/19 → 15/01/19 |
Fingerprint
Keywords
- formal proof
- Hensel's lemma
- Lean
- p-adic
Cite this
}
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 proceeding › Conference contribution › Academic › peer-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 -