2026-07-072026-07-07http://salesiana.dossiersoluciones.com/handle/123456789/72816An 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.Algebraic GeometryFormalized proof, computation, and the construction problem in algebraic geometrytext