  We report on a formalization of schemes in the proof assistant Isabelle/HOL,
and we discuss the design choices made in the process. Schemes are
sophisticated mathematical objects in algebraic geometry introduced by
Alexander Grothendieck in 1960. This experiment shows that the simple type
theory implemented in Isabelle can handle such elaborate constructions despite
doubts raised about Isabelle's capability in that direction. We show in the
particular case of schemes how the powerful dependent types of Coq or Lean can
be traded for a minimalist apparatus called locales.
