🐙Lean & Math-AI Seminar
Title: Opportunities in Math-AI and Lean-Math-AI
Speaker: Ashvni Narayanan, SMRI, Sydney, Australia
Date: Wed, 23 Apr 2025
Time: 4 pm
Venue: LH-3, Mathematics Department
Title: Lean for Teaching
Speaker: Patrick Massot, Université Paris-Saclay, Saint-Aubin, France
Date: Tue, 22 Apr 2025
Time: 4 pm
Venue: LH-3, Mathematics Department
I will describe how the Lean proof assistant software can be used to teach mathematical reasoning to young students at university. This is different from teaching how to use Lean. Here Lean is only a tool, not the end goal.
I will explain what we can hope to teach using this tool, what are the available resources for teachers, and what choices should be made. I will then show my teaching library, Verbose Lean, which uses controlled natural language and customizable automation to optimize transfer of skills to paper proofs.
Title: Certifying Algebraic Number Theory Computation
Speaker: Anne Baanen, Lean FRO
Date: Tue, 22 Apr 2025
Time: 11 am
Venue: LH-3, Mathematics Department (Joint with the Number Theory Seminar)
Number fields and their rings of integers are fundamental objects in algebraic number theory. Computational information on these objects is available in computer algebra systems and databases. To make these values available to formalization in Lean 4, without tediously redoing existing work, we developed a variety of certificates that allow Lean to efficiently verify the outcome of computations. In particular I will focus on computing and certifying the ring of integers. The work of this talk is joint with Alain Chavarri Villarello and Sander Dahmen at Vrije Universiteit Amsterdam.
Title: Formalization of $p$-adic $L$-functions in Lean 3
Speaker: Ashvni Narayanan (London school of Geometry and Number Theory; Sydney University)
Date: Wed, 13 Sep 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.