Algebraic Geometry in Mathlib

Add to your list(s) Download to your calendar using vCal

• Andrew Yang (Imperial College, London)
• Thursday 08 May 2025, 17:00-18:00
• MR14 Centre for Mathematical Sciences.

If you have a question about this talk, please contact Anand Rao Tadipatri.

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

This talk is part of the Formalisation of mathematics with interactive theorem provers series.

This talk is included in these lists:

• All CMS events
• All Talks (aka the CURE list)
• CMS Events
• Cambridge talks
• DPMMS Lists
• DPMMS Pure Maths study groups
• DPMMS info aggregator
• DPMMS lists
• Department of Computer Science and Technology talks and seminars
• Formalisation of mathematics with interactive theorem provers
• Hanchen DaDaDash
• Interested Talks
• MR14 Centre for Mathematical Sciences
• School of Physical Sciences
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.