|
| 1 | +--- |
| 2 | +author: 'Harald Carlens' |
| 3 | +category: 'meeting report' |
| 4 | +date: 2024-11-23 13:00:00 UTC+02:00 |
| 5 | +description: 'A week at the computational algebraic geometry workshop in Durham.' |
| 6 | +has_math: true |
| 7 | +link: '' |
| 8 | +slug: durham-algebraic-geometry-workshop |
| 9 | +tags: '' |
| 10 | +title: Durham Computational Algebraic Geometry Workshop |
| 11 | +type: text |
| 12 | +--- |
| 13 | + |
| 14 | +A group effort to formalise some algebraic geometry in Lean. |
| 15 | + |
| 16 | +<!-- TEASER_END --> |
| 17 | + |
| 18 | +I found out about the 2024 [Durham Computational Algebraic Geometry workshop](https://sites.google.com/view/durhamcompalggeom/home) |
| 19 | +through the |
| 20 | +[Lean events page](https://leanprover-community.github.io/events.html). I'd been learning Lean in my spare time, having |
| 21 | +worked through the natural numbers game and some of the textbook resources after first encountering Lean through the |
| 22 | +machine learning theorem proving community, and was interested to see how formalisation happens in practice. |
| 23 | + |
| 24 | +# Workshop |
| 25 | + |
| 26 | +The week-long workshop was broader than formalisation. It also included interesting talks on |
| 27 | +[Macaulay2](http://www2.macaulay2.com/Macaulay2/) and [Oscar](https://oscar.computeralgebra.de/), and groups working |
| 28 | +on projects using those languages. |
| 29 | + |
| 30 | +Of the roughly 20 people at the workshop, our Lean group was made up of 8 people with a wide range of Lean experience |
| 31 | +— including people who had never written a line of Lean before, recovering Mathlib contributors, Lean PhDs, and |
| 32 | +Kevin Buzzard. |
| 33 | + |
| 34 | +# Project |
| 35 | + |
| 36 | +Kevin and his two PhD students had chosen a project that they thought might be doable in a week: to use the |
| 37 | +recently-formalised valuative criterion to formalise the proof that Proj of a graded ring is separated and proper. |
| 38 | +As a fundamental result in algebraic geometry, this would be a small part of the basic machinery needed to make progress |
| 39 | +on the proof of Fermat's Last Theorem. |
| 40 | + |
| 41 | +Though it is a statement about schemes, Kevin and his PhD students managed to abstract away much of the scheme theory |
| 42 | +and leave us proving a statement about commutative algebra. |
| 43 | + |
| 44 | +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 |
| 45 | +student or researcher, I went to the workshop expecting to mostly be a passive observer. I was very grateful to the rest |
| 46 | +of the group who were extremely patient in explaining some of the maths to me, and gained a real appreciation for some |
| 47 | +of the difficulties in porting "obvious" blackboard statements from chalk into Lean. |
| 48 | + |
| 49 | + |
| 50 | + |
| 51 | +# Formalisation in practice |
| 52 | + |
| 53 | +We spent the first two days working together as one group, taking turns screen-sharing and editing our proof attempt |
| 54 | +with help from everyone. |
| 55 | + |
| 56 | +By Thursday, we'd proved separatedness — and |
| 57 | +[the PR containing our proof was merged into Mathlib](https://github.com/leanprover-community/mathlib4/pull/19290). |
| 58 | + |
| 59 | +We'd also formalised the statement for properness, and had a sketch for the proof of properness containing lots of |
| 60 | +`sorry`s. We split into groups to tackle these in parallel. |
| 61 | + |
| 62 | +This collaboration was made much easier by the real-time feedback from Lean on our progress, though at times we found |
| 63 | +that we needed to change some of our theorem statements and assumptions, which required larger refactors of the work |
| 64 | +we'd already done. |
| 65 | + |
| 66 | +The group used the Stacks project as a guide, and in the process of formalisation discovered a small |
| 67 | +algebraic error in the [Stacks project proof](https://stacks.math.columbia.edu/tag/01MF). Details of the error[^hint] |
| 68 | +are left as an exercise to the reader! |
| 69 | + |
| 70 | +Some of the things that slowed us down were dealing with edge cases that seem non-material, like dealing with the zero |
| 71 | +ring, or actually formalising something that just looks like the obvious identity map when written informally, and |
| 72 | +choosing the most useful definition of finiteness out of a few options in Mathlib. |
| 73 | + |
| 74 | +When proving theorems in Lean, one encounters some of the same addictive elements as when playing a game. |
| 75 | +On Thursday afternoon it seemed unlikely we'd |
| 76 | +finish in time for the end of the workshop, but after some evening pizza in the maths department and several "last |
| 77 | +`sorry` before we leave"s (as well as lots of overnight work from Kevin and Andrew), we got a completed proof just in |
| 78 | +time to present to the other groups. |
| 79 | + |
| 80 | +# Conclusion |
| 81 | + |
| 82 | +Throughout this week, I felt like I got a great insight into what formalising mathematics looks like in practice. |
| 83 | +As well as each of our own efforts at contributing to the formal proof, I and others in the group also learnt a lot from |
| 84 | +the interactions between Kevin and his PhD students, especially in terms of the design considerations behind even a |
| 85 | +relatively small project like this. |
| 86 | + |
| 87 | +Once we had formalised the statements we wanted to prove, we were able to split into groups and attack them in parallel. |
| 88 | +But it was this initial formalisation of the statements that felt in some ways more impactful, and choosing the right |
| 89 | +definitions — both in terms of facilitating the Lean proof for them, and making them useful for |
| 90 | +downstream users — took quite some time and effort. |
| 91 | + |
| 92 | +A few of us who met this week are planning to stay in touch and keep learning Lean together. We hope to |
| 93 | +see you on [Zulip](https://leanprover.zulipchat.com/)! |
| 94 | + |
| 95 | +_Our group was made up of Patience Ablett, Kevin Buzzard, Harald Carlens, Wayne Ng Kwing King, Michael Schlößer, |
| 96 | +Justus Springer, Andrew Yang, and Jujian Zhang. The commit history is in |
| 97 | +[this separate repo](https://github.com/kbuzzard/DurhamAlgGeom2024) used throughout the workshop. |
| 98 | +(commit author doesn't mean code author; work was done in collaboration)_ |
| 99 | + |
| 100 | +[^hint]: There is a $d$ in the definition of $\gamma_{i}$ — but where is it in the chain of inequalities? |
0 commit comments