at the

American Institute of Mathematics, Pasadena, California

organized by

Kevin Buzzard, Johan Commelin, Joel Riou, and Adam Topaz

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.