# Formalization of $p$-adic $L$-functions in Lean 3

## TL;DR

This paper formalizes the concept of $p$-adic $L$-functions within Lean 3, including their properties and special values, marking a novel achievement in theorem proving for number theory.

## Contribution

It is the first formalization of $p$-adic $L$-functions in a theorem prover, involving extensive formalization of related mathematical concepts.

## Key findings

- Formalization of $p$-adic $L$-functions in Lean 3.
- Proof that these functions take expected values at negative integers.
- Implementation supported by Lean's mathlib library.

## Abstract

The Euler--Riemann zeta function is a largely studied numbertheoretic object, and the birthplace of several conjectures, such as the Riemann Hypothesis. Different approaches are used to study it, including $p$-adic analysis : deriving information from $p$-adic zeta functions. A generalized version of $p$-adic zeta functions (Riemann zeta function) are $p$-adic $L$-functions (resp. Dirichlet $L$-functions). This paper describes formalization of $p$-adic $L$-functions in an interactive theorem prover Lean 3. Kubota--Leopoldt $p$-adic $L$-functions are meromorphic functions emerging from the special values they take at negative integers in terms of generalized Bernoulli numbers. They also take twisted values of the Dirichlet $L$-function at negative integers. This work has never been done before in any theorem prover. Our work is done with the support of \lean{mathlib} 3, one of Lean's mathematical libraries. It required formalization of a lot of associated topics, such as Dirichlet characters, Bernoulli polynomials etc. We formalize these first, then the definition of a $p$-adic $L$-function in terms of an integral with respect to the Bernoulli measure, proving that they take the required values at negative integers.