Kevin Buzzard,
Johan Commelin,
Joel Riou,
and Adam Topaz
Original Announcement
This workshop will be devoted to formalising basic and advanced concepts in algebraic geometry. Algebraic geometry should be interpreted broadly, and could include topics in related areas such as complex differential geometry and arithmetic geometry. Formalising here means translating mathematical ideas into the language of a computer theorem prover; the prover we will use will be Lean. Works such as EGA and the Stacks project are comprehensive human-written sources for modern algebraic geometry, however they are huge and need to be triaged before a comprehensive formalisation can take place.
The main topics for the workshop are:
Isolation of key formalisable goals in the area;
Developing strategies to formalise key definitions and theorems (for example the Riemann-Roch theorem and its generalisations, definitions and basic facts about coherent and etale cohomology, faithfully flat descent, etale fundemantal group ...);
Formalising these definitions and theorems, and PRing the work to Lean's mathematics libary;
Development of a blueprint for future progress in the area.