{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:30:40Z","timestamp":1750221040756,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":35,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,1,14]],"date-time":"2019-01-14T00:00:00Z","timestamp":1547424000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100010663","name":"European Research Council","doi-asserted-by":"publisher","award":["713999"],"award-info":[{"award-number":["713999"]}],"id":[{"id":"10.13039\/100010663","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,1,14]]},"DOI":"10.1145\/3293880.3294089","type":"proceedings-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:56Z","timestamp":1546608836000},"page":"15-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["A formal proof of Hensel's lemma over the p-adic integers"],"prefix":"10.1145","author":[{"given":"Robert Y.","family":"Lewis","sequence":"first","affiliation":[{"name":"Vrije Universiteit Amsterdam, Netherlands"}]}],"member":"320","published-online":{"date-parts":[[2019,1,14]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297658.1297660"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-015-9356-y"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9440-6"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Evmorfia-Iro Bartzia and Pierre-Yves Strub. 2014. A Formal Library for Elliptic Curves in the Coq Proof Assistant. In Interactive Theorem Proving Gerwin Klein and Ruben Gamboa (Eds.). Springer International Publishing Cham 77\u201392.  Evmorfia-Iro Bartzia and Pierre-Yves Strub. 2014. A Formal Library for Elliptic Curves in the Coq Proof Assistant. In Interactive Theorem Proving Gerwin Klein and Ruben Gamboa (Eds.). Springer International Publishing Cham 77\u201392.","DOI":"10.1007\/978-3-319-08970-6_6"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854065.2854072"},{"key":"e_1_3_2_1_6_1","unstructured":"Nicolas Bourbaki. 1998. General topology. Chapters 1\u20134. Springer Berlin. vii+437 pages. Translated from the French Reprint of the 1989 English translation.  Nicolas Bourbaki. 1998. General topology. Chapters 1\u20134. Springer Berlin. vii+437 pages. Translated from the French Reprint of the 1989 English translation."},{"key":"e_1_3_2_1_7_1","volume-title":"Proc. Sympos. Pure Math.","volume":"97","author":"Browning T. D.","year":"2018"},{"volume-title":"Proceedings of the 9th Conference on Intelligent Computer Mathematics (CICM","year":"2016","author":"Carneiro Mario","key":"e_1_3_2_1_8_1"},{"key":"e_1_3_2_1_9_1","unstructured":"Mario Carneiro. 2018. The Lean 3 Mathematical Library (presentation). http:\/\/robertylewis.com\/files\/icms\/Carneiro_mathlib.pdf  Mario Carneiro. 2018. The Lean 3 Mathematical Library (presentation). http:\/\/robertylewis.com\/files\/icms\/Carneiro_mathlib.pdf"},{"volume-title":"COLOG-88 (Tallinn","year":"1988","author":"Coquand Thierry","key":"e_1_3_2_1_10_1"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.4064\/aa164-1-5"},{"key":"e_1_3_2_1_12_1","unstructured":"Leonardo de Moura Gabriel Ebner Jared Roesch and Sebastian Ullrich. 2017. The Lean Theorem Prover (presentation). http:\/\/leanprover. github.io\/presentations\/20170116_POPL  Leonardo de Moura Gabriel Ebner Jared Roesch and Sebastian Ullrich. 2017. The Lean Theorem Prover (presentation). http:\/\/leanprover. github.io\/presentations\/20170116_POPL"},{"key":"e_1_3_2_1_13_1","unstructured":"Leonardo de Moura Soonho Kong Jeremy Avigad Floris van Doorn and Jakob von Raumer. 2014. The Lean Theorem Prover. http:\/\/leanprover.github.io\/files\/system.pdf (2014).  Leonardo de Moura Soonho Kong Jeremy Avigad Floris van Doorn and Jakob von Raumer. 2014. The Lean Theorem Prover. http:\/\/leanprover.github.io\/files\/system.pdf (2014)."},{"key":"e_1_3_2_1_14_1","unstructured":"Manuel Eberl. 2017. Dirichlet L-Functions and Dirichlet\u2019s Theorem. Archive of Formal Proofs (Dec. 2017). http:\/\/isa-afp.org\/entries\/ Dirichlet_L.html Formal proof development.  Manuel Eberl. 2017. Dirichlet L-Functions and Dirichlet\u2019s Theorem. Archive of Formal Proofs (Dec. 2017). http:\/\/isa-afp.org\/entries\/ Dirichlet_L.html Formal proof development."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110278"},{"key":"e_1_3_2_1_16_1","first-page":"1382","article-title":"Formal proof\u2013the four-color theorem","volume":"55","author":"Gonthier Georges","year":"2008","journal-title":"Notices of the AMS"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_14"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"crossref","unstructured":"Fernando Q. Gouv\u00eaa. 1997. p-adic Numbers (second ed.). Springer Berlin. vi+298 pages.  Fernando Q. Gouv\u00eaa. 1997. p-adic Numbers (second ed.). Springer Berlin. vi+298 pages.","DOI":"10.1007\/978-3-642-59058-0"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_7"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1017\/fmp.2017.1"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9145-6"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1137\/0208011"},{"key":"e_1_3_2_1_23_1","unstructured":"Kurt Hensel. 1908. Theorie der algebraischen Zahlen. Number v. 1 in Cornell University Library historical math monographs. B. G. Teubner. https:\/\/books.google.nl\/books?id=CHUAAAAAMAAJ  Kurt Hensel. 1908. Theorie der algebraischen Zahlen. Number v. 1 in Cornell University Library historical math monographs. B. G. Teubner. https:\/\/books.google.nl\/books?id=CHUAAAAAMAAJ"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_21"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"crossref","unstructured":"Ioan James. 1999. Topologies and uniformities. Springer-Verlag London Ltd. London. xvi+230 pages.  Ioan James. 1999. Topologies and uniformities. Springer-Verlag London Ltd. London. xvi+230 pages.","DOI":"10.1007\/978-1-4471-3994-2"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"crossref","unstructured":"Christer Lech. 1953. A note on recurring series. Ark. Mat. 2 5 (08 1953) 417\u2013421.  Christer Lech. 1953. A note on recurring series. Ark. Mat. 2 5 (08 1953) 417\u2013421.","DOI":"10.1007\/BF02590997"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.262.4"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1515\/crll.1958.199.23","article-title":"An interpolation series for continuous functions of a p-adic variable","volume":"199","author":"Mahler K.","year":"1958","journal-title":"J. Reine Angew. Math."},{"key":"e_1_3_2_1_29_1","first-page":"99","article-title":"The method of Chabauty and Coleman. In Explicit methods in number theory. Panor. Synth\u00e8ses, Vol. 36","author":"McCallum William","year":"2012","journal-title":"Soc. Math. France, Paris"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"crossref","unstructured":"Norman Megill. 2006. Metamath. The Seventeen Provers of the World (2006) 88\u201395.   Norman Megill. 2006. Metamath. The Seventeen Provers of the World (2006) 88\u201395.","DOI":"10.1007\/11542384_13"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02422947"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"crossref","unstructured":"J.-P. Serre. 1973. A course in arithmetic. Springer-Verlag New YorkHeidelberg. viii+115 pages. Translated from the French Graduate Texts in Mathematics No. 7.  J.-P. Serre. 1973. A course in arithmetic. Springer-Verlag New YorkHeidelberg. viii+115 pages. Translated from the French Graduate Texts in Mathematics No. 7.","DOI":"10.1007\/978-1-4684-9884-4"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129511000119"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"crossref","unstructured":"Floris van Doorn Jakob von Raumer and Ulrik Buchholtz. 2017. Homotopy Type Theory in Lean. Springer International Publishing Cham 479\u2013495.  Floris van Doorn Jakob von Raumer and Ulrik Buchholtz. 2017. Homotopy Type Theory in Lean. Springer International Publishing Cham 479\u2013495.","DOI":"10.1007\/978-3-319-66107-0_30"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75283"}],"event":{"name":"CPP '19: 8th ACM SIGPLAN International Conference on Certified Programs and Proofs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"],"location":"Cascais Portugal","acronym":"CPP '19"},"container-title":["Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3293880.3294089","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3293880.3294089","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:43:49Z","timestamp":1750207429000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3293880.3294089"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,14]]},"references-count":35,"alternative-id":["10.1145\/3293880.3294089","10.1145\/3293880"],"URL":"https:\/\/doi.org\/10.1145\/3293880.3294089","relation":{},"subject":[],"published":{"date-parts":[[2019,1,14]]},"assertion":[{"value":"2019-01-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}