BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Algebraic Geometry in Mathlib - Andrew Yang (Imperial College\, Lo
 ndon)
DTSTART:20250508T160000Z
DTEND:20250508T170000Z
UID:TALK225409@talks.cam.ac.uk
CONTACT:Anand Rao Tadipatri
DESCRIPTION:Algebraic geometry is the study of systems of polynomial equat
 ions\, and more broadly\, the interplay between commutative algebra and ge
 ometry. It is a field with a rich history and a modern foundation\, drawin
 g 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 over
 view of the current state of the library\, highlighting key developments\,
  challenges encountered along the way\, and the solutions we have adopted.
 \n\n=== Hybrid talk ===\n\nJoin Zoom Meeting\nhttps://cam-ac-uk.zoom.us/j/
 89856091954?pwd=Bba77QB2KuTideTlH6PjAmbXLO8HbY.1\n\nMeeting ID: 898 5609 1
 954\nPasscode: ITPtalk
LOCATION:MR14 Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR