Formalized proof, computation, and the construction problem in algebraic geometry

TL;DR

This paper discusses how the construction problem in algebraic geometry motivates the development of formal proof methods and shares progress on formalizing category theory within a ZFC-like framework.

Contribution

It introduces the motivation for formal proof methods in algebraic geometry and reports progress on formalizing category theory in a set-theoretic environment.

Findings

Formal proof methods are motivated by the construction problem in algebraic geometry.

Progress has been made in formalizing category theory within a ZFC-like system.

The discussion highlights the potential of formalization to advance algebraic geometry.

Abstract

An informal discussion of how the construction problem in algebraic geometry motivates the search for formal proof methods. Also includes a brief discussion of my own progress up to now, which concerns the formalization of category theory within a ZFC-like environment.