Type: Seminar

Distribution: World

Expiry: 8 Jan 2024

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

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.

Calendar (ICS file) download, for import into your favourite calendar application

UNCLUTTER for printing

AUTHENTICATE to mark the scnews item as read