Tuesday, 4-June-2024 


The Kubota-Leopoldt p-adic L-function is an important concept in number theory. It takes special values in terms of generalized Bernoulli numbers and helps solve Kummer congruences. It is also used in Iwasawa theory. Formalization of p-adic L-functions has been done for the first time in a theorem prover called Lean 3. In this talk, we shall briefly introduce the concept of formalization of mathematics in Lean, the theory behind p-adic L-functions, and its formalization.


Ashvni Narayanan 

Research area

Pure Mathematics


University of Sydney


Tuesday 4 June 2024, 12:05 pm


Room 4082, Anita B. Lawrence