University of Cambridge > Talks.cam > Formalisation of mathematics with interactive theorem provers > Algebraic Geometry in Mathlib

  Browse A-Z

Log in

Googledetails Microsoftdetails

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹī¸ Information

Algebraic Geometry in Mathlib

Download to your calendar using vCal

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:

Note that ex-directory lists are not shown.

Other lists

Battcock, Room location TBA Seminar Room SG1, Alison Richard Building, 7 West Road, Cambridge CB3 9DT Chemistry Dept, Unilever Lecture Theatre and Teams

Other talks

Quantifying the unquantifiable? Assessing the importance of almsgiving in early modern France and Spain Tissue-scale communication in cancer development Director's Welcome Online Causal Inference Seminar Title to be confirmed Title to be confirmed
 

Š 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity