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