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

Linfoot Number Theory Seminar

26th January 2022, 11:00 am – 12:00 pm

Fry Building, 4th Floor Seminar Room

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.

## Comments are closed.