Schemes in Lean

Abstract

We tell the story of how schemes were formalized in three different ways in the Lean theorem prover.

Keywords:

• Scheme
• lean
• formal proof

Acknowledgments

We are very grateful to Mario Carneiro, Reid Barton and Neil Strickland, all of whom provided major insights to help us on our way.

Declaration of Interest

No potential conflict of interest was reported by the author(s).

Notes

1 Note that Whitney had defined an abstract real manifold ten years earlier in [10], by gluing together open subsets of Euclidean space in the now familiar way.

2 The Stacks project [8] covers a huge swathe of algebraic geometry and its prerequisites. As the project was largely a collaboration by KB with undergraduates, the fact that the Stacks project is freely available online was helpful as it was accessible to everyone. Moreover, the Stacks project is careful to use “Tags,” which never change, to refer to particular theorems or sections of the material, so it is easy to cross-reference.

3 Strictly speaking we needed a little more than this; in our situation $f_i\in R[1/f]$ rather than R, however this special case (a cover of U coming from a cover of X) is already enough to illustrate the problem we had.

4 note now that the proof has been changed; the proof formalised in our project is the one from algebra.tex in the Stacks project as it stood in late 2017 after commit 39135dd.

Additional information

Funding

The first author was supported in part by EPSRC grant EP/L025485/1. Scott Morrison was supported in part by Australian Research Council grant ARC DP200100067.