Add to Outlook calendar Add to Google calendar
Title: Formalization of $p$-adic $L$-functions in Lean 3
Speaker: Ashvni Narayanan (London school of Geometry and Number Theory; Sydney University)
Date: 13 September 2023
Time: 4:00 pm
Venue: LH-1, Mathematics Department

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.


Contact: +91 (80) 2293 2711, +91 (80) 2293 2265 ;     E-mail: chair.math[at]iisc[dot]ac[dot]in
Last updated: 29 Feb 2024