9th May: Ashvni Narayanan

Title : Formalization of pp-adic LL-functions in Lean

Abstract : pp-adic LL-functions arose out of the study of Kummer congruences and Dirichlet LL-functions. Their values at negative integers are related to generalized Bernoulli numbers. We shall explain their construction in the theorem prover Lean. After a brief introduction to Lean, we shall delve into the construction of Dirichlet characters, Bernoulli numbers, and other supporting objects. We will then get to the non canonical definition of the pp-adic LL-function in Lean in terms of a pp-adic integral. If time permits, we will also discuss properties and evaluation at negative integers.