Formalization of p-adic L- functions in Lean, and auto formalization as a mathematical tool
Time: 2024-01-22
Published By: Yiyi Ye
Speaker(s): Ashvni Narayanan(University of Sydney)
Time: 10:00-12:00 January 23, 2024
Venue: Lecture Hall, Jiayibing Building, Jingchunyuan 82, BICMR
Abstract :
L-functions are an integral part of number theory. We discuss formalization of their p-adic analogue. We shall also discuss a tool which translates natural language to Lean code.
