From 1caefe716f0ef092aa4dcf119e17cd042ff07423 Mon Sep 17 00:00:00 2001 From: harald Date: Mon, 25 Nov 2024 17:26:50 +0000 Subject: [PATCH] Tweaks to Durham post --- posts/durham-algebraic-geometry-workshop.md | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/posts/durham-algebraic-geometry-workshop.md b/posts/durham-algebraic-geometry-workshop.md index f7b80d69..b19e7f2c 100644 --- a/posts/durham-algebraic-geometry-workshop.md +++ b/posts/durham-algebraic-geometry-workshop.md @@ -1,7 +1,7 @@ --- author: 'Harald Carlens' category: 'meeting report' -date: 2024-11-23 13:00:00 UTC+02:00 +date: 2024-11-25 17:00:00 UTC+00:00 description: 'A week at the computational algebraic geometry workshop in Durham.' has_math: true link: '' @@ -33,13 +33,14 @@ Kevin Buzzard. # Project -Kevin and his two PhD students had chosen a project that they thought might be doable in a week: to use the +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 and his PhD students managed to abstract away much of the scheme theory -and leave us proving a statement about commutative algebra. +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 @@ -80,9 +81,8 @@ 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. -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 -the interactions between Kevin and his PhD students, especially in terms of the design considerations behind even a -relatively small project like this. +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