## 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/Territory | Portugal |

City | Cascais |

Period | 14/01/19 → 15/01/19 |

## Keywords

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