BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Formalisation of mathematics with interactive theo
 rem provers 
SUMMARY:Algebraic Geometry in Mathlib - Andrew Yang (Imper
 ial College\, London)
DTSTART;TZID=Europe/London:20250508T170000
DTEND;TZID=Europe/London:20250508T180000
UID:TALK225409AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/225409
DESCRIPTION:Algebraic geometry is the study of systems of poly
 nomial equations\, and more broadly\, the interpla
 y between commutative algebra and geometry. It is 
 a field with a rich history and a modern foundatio
 n\, drawing heavily on ring theory\, topology\, an
 d category theory. Over the years\, mathlib\, the 
 Lean 4 library of formalized mathematics\, has dev
 eloped a sizable body of algebraic geometry. In th
 is talk\, I will present an overview of the curren
 t state of the library\, highlighting key developm
 ents\, challenges encountered along the way\, and 
 the solutions we have adopted.\n\n=== Hybrid talk 
 ===\n\nJoin Zoom Meeting\nhttps://cam-ac-uk.zoom.u
 s/j/89856091954?pwd=Bba77QB2KuTideTlH6PjAmbXLO8HbY
 .1\n\nMeeting ID: 898 5609 1954\nPasscode: ITPtalk
LOCATION:MR14 Centre for Mathematical Sciences
CONTACT:Anand Rao Tadipatri
END:VEVENT
END:VCALENDAR