A group effort to formalise some algebraic geometry in Lean.

I found out about the 2024 Durham Computational Algebraic Geometry workshop through the Lean events page. I'd been learning Lean in my spare time, having worked through the natural numbers game and some of the textbook resources after first encountering Lean through the machine learning theorem proving community, and was interested to see how formalisation happens in practice.

Workshop

The week-long workshop was broader than formalisation. It also included interesting talks on Macaulay2 and Oscar, and groups working on projects using those languages.

Of the roughly 20 people at the workshop, our Lean group was made up of 8 people with a wide range of Lean experience — including people who had never written a line of Lean before, recovering Mathlib contributors, Lean PhDs, and Kevin Buzzard.

Project

Kevin and his two PhD students, Andrew Yang and Jujian Zhang, had chosen a project that they thought might be doable in a week: to use the recently-formalised valuative criterion to formalise the proof that Proj of a graded ring is separated and proper. As a fundamental result in algebraic geometry, this would be a small part of the basic machinery needed to make progress on the proof of Fermat's Last Theorem.

Though it is a statement about schemes, Kevin, Andrew and Jujian managed to abstract away much of the scheme theory, leaving us to prove a statement about commutative algebra.

As a bit of an outsider in the group (with a decade-old BA in mathematics), and the only member who was not a PhD student or researcher, I went to the workshop expecting to mostly be a passive observer. I was very grateful to the rest of the group who were extremely patient in explaining some of the maths to me, and gained a real appreciation for some of the difficulties in porting "obvious" blackboard statements from chalk into Lean.

Formalisation in practice

We spent the first two days working together as one group, taking turns screen-sharing and editing our proof attempt with help from everyone.

By Thursday, we'd proved separatedness — and the PR containing our proof was merged into Mathlib.

We'd also formalised the statement for properness, and had a sketch for the proof of properness containing lots of sorrys. We split into groups to tackle these in parallel.

This collaboration was made much easier by the real-time feedback from Lean on our progress, though at times we found that we needed to change some of our theorem statements and assumptions, which required larger refactors of the work we'd already done.

The group used the Stacks project as a guide, and in the process of formalisation discovered a small algebraic error in the Stacks project proof. Details of the error¹ are left as an exercise to the reader!

Some of the things that slowed us down were dealing with edge cases that seem non-material, like dealing with the zero ring, or actually formalising something that just looks like the obvious identity map when written informally, and choosing the most useful definition of finiteness out of a few options in Mathlib.

When proving theorems in Lean, one encounters some of the same addictive elements as when playing a game. On Thursday afternoon it seemed unlikely we'd finish in time for the end of the workshop, but after some evening pizza in the maths department and several "last sorry before we leave"s (as well as lots of overnight work from Kevin and Andrew), we got a completed proof just in time to present to the other groups.

Conclusion

Throughout this week, I felt like I got a great insight into what formalising mathematics looks like in practice. The discussions between the more experienced members of the group were illuminating, especially in terms of the design considerations behind even a relatively small project like this.

Once we had formalised the statements we wanted to prove, we were able to split into groups and attack them in parallel. But it was this initial formalisation of the statements that felt in some ways more impactful, and choosing the right definitions — both in terms of facilitating the Lean proof for them, and making them useful for downstream users — took quite some time and effort.

A few of us who met this week are planning to stay in touch and keep learning Lean together. We hope to see you on Zulip!

Our group was made up of Patience Ablett, Kevin Buzzard, Harald Carlens, Wayne Ng Kwing King, Michael Schlößer, Justus Springer, Andrew Yang, and Jujian Zhang. The commit history is in this separate repo used throughout the workshop. (commit author doesn't mean code author; work was done in collaboration)