SMS scnews item created by Alex Sherman at Mon 30 Oct 2023 1159
Type: Seminar
Distribution: World
Expiry: 8 Jan 2024
Calendar1: 3 Nov 2023 1200-1300
CalLoc1: Carslaw 173
CalTitle1: Algebra Seminar: Formalization of p-adic L-functions in Lean 3
Auth: alexs@desktop-h8gjltm.staff.wireless.sydney.edu.au (ashe8718) in SMS-SAML

Algebra Seminar: Narayanan -- Formalization of p-adic L-functions in Lean 3

Ashvni Narayanan (University of Sydney) is speaking in the Algebra Seminar this week.
We will go out for lunch after the talk.  

When: Friday, 3 November, 12-1pm 

Where: Carslaw 173 

Title : Formalization of p-adic L-functions in Lean 3 

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, the theory
behind p-adic L-functions, and its formalization.