Ashvni Narayanan

Formalization of p-adic measure theory and p-adic L-functions in Lean

p-adic measure theory plays an important role in stating and proving the Iwasawa Main Conjecture. In this talk, I will connect the p-adic integral to the Kubota-Leopoldt L-function. I will also explain how these concepts have been formalized in the interactive theorem prover Lean.