skip to content

Department of Computer Science and Technology

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

Upcoming seminars