**This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.**

### Abstract

We formalize mainstream structures in algebraic geometry culminating
in Grothendieck's schemes: presheaves of rings, sheaves of rings,
ringed spaces, locally ringed spaces, affine schemes and schemes. We
prove that the spectrum of a ring is a locally ringed space, hence an
affine scheme. Finally, we prove that any affine scheme is a scheme.