Date:
Thursday, 8 May, 2025 - 17:00 to 18:00
Speaker:
Andrew Yang (Imperial College, London)
Venue:
MR14 Centre for Mathematical Sciences
Algebraic geometry is the study of systems of polynomial equations, and more broadly, the interplay between commutative algebra and geometry. It is a field with a rich history and a modern foundation, drawing heavily on ring theory, topology, and category theory. Over the years, mathlib, the Lean 4 library of formalized mathematics, has developed a sizable body of algebraic geometry. In this talk, I will present an overview of the current state of the library, highlighting key developments, challenges encountered along the way, and the solutions we have adopted.
=== Hybrid talk ===
Join Zoom Meeting
https://cam-ac-uk.zoom.us/j/89856091954?pwd=Bba77QB2KuTideTlH6PjAmbXLO8HbY.1
Meeting ID: 898 5609 1954
Passcode: ITPtalk
Seminar series:
Formalisation of mathematics with interactive theorem provers
