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

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

*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

}

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

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 -