Algebraic Geometry

Stream: new members

[Andreas Vollert]

Hi everyone. I’m a math and computer science student at the Technical University of Munich, working on a project with Prof. Christian Liedtke. We’re trying to get a sense of how mathlib covers algebraic geometry and how people are using it. My goal is to put together a guide that helps someone with no experience in theorem provers get to the point where they can play around with the algebraic geometry part of mathlib. Ideally, I’d also like to contribute something back to mathlib along the way.

I’ve used Isabelle quite a bit before and have gone through Mathematics in Lean. Right now I’m exploring the definitions of schemes, sheaves, functors, etc., and getting a feel for how they fit together.

Are there any relatively low-hanging fruits in this area of mathlib that would be good starting points?

[Kenny Lau]

Andreas Vollert said:

someone with no experience in theorem provers get to the point where they can play around with the algebraic geometry part of mathlib

surely doing anything in Lean requires experience in Lean

[Andreas Vollert]

I'll include the minimal necessary basics for Lean

[Yan Yablonovskiy 🇺🇦]

Andreas Vollert said:

Hi everyone. I’m a math and computer science student at the Technical University of Munich, working on a project with Prof. Christian Liedtke. We’re trying to get a sense of how mathlib covers algebraic geometry and how people are using it. My goal is to put together a guide that helps someone with no experience in theorem provers get to the point where they can play around with the algebraic geometry part of mathlib. Ideally, I’d also like to contribute something back to mathlib along the way.

I’ve used Isabelle quite a bit before and have gone through Mathematics in Lean. Right now I’m exploring the definitions of schemes, sheaves, functors, etc., and getting a feel for how they fit together.

Are there any relatively low-hanging fruits in this area of mathlib that would be good starting points?

I would recommend choosing your favourite (rather rigorous text) and cross-referencing any results that are in mathlib (since it is a learning exercise) . Better yet, try build up an API yourself, from some mathlib starting point, and check with the Mathlib version as a solution guide of sorts.

[Kevin Buzzard]

I think that there is a gap in the market here. It would be a really interesting challenge to start off with someone who has done little more than played NNG but knows the mathematical basics of schemes/sheaves and take them on a tour of what we have.