The Stacks Project is an extensive open-source textbook and reference work focused on algebraic geometry and related fields. Each lemma, theorem, definition, remark, example, and other significant items within the project is assigned a unique tag, with the current scope of the project including more than 21000 tags.

This question resolves to the first year in which at least 11000 tags of the stacks project have been formalized in a proof assistant such as Lean, Coq, Isabelle, etc. It resolves to the last option (2030 or later) if no such milestone has been reached by the end of 2029.

Further information on resolution criteria:

• I consider it to be almost certain that a formalization as above will require a concerted project which includes a mechanism to track the progress on the number of formalized tags. If such a project is created, this would be used to determine the year of resolution above.

• If there is an effort to formalize algebraic geometry based on some other resource (such as EGA) I would exercise my best judgement to determine when that project covers the majority of the results appearing in the Stacks project. This would include consulting with the project leads and experts in algebraic geometry such as Aise Johan de Jong or Ravi Vakil.