Formalization of p-adic L-functions in Lean 3

Tuesday, 4-June-2024 

Abstract

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.