Formalising algebraic geometry

Formalising algebraic geometry

This online workshop, sponsored by AIM and the NSF, 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.

This event will be run as an AIM-style workshop. Participants will be invited to suggest open problems and questions before the workshop begins, and these will be posted on the workshop website. These include specific problems on which there is hope of making some progress during the workshop, as well as more ambitious problems which may influence the future activity of the field. Lectures at the workshop will be focused on familiarizing the participants with the background material leading up to specific problems, and the schedule will include discussion and parallel working sessions.

The deadline to apply for support to participate in this workshop has passed.

For more information email workshops@aimath.org

Plain text announcement or brief announcement.