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

2004/10/08 by Carlos T. Simpson, Simpson, Carlos T.
Mathematics · #Algebraic Geometry (math.AG) #FOS: Mathematics #math.AG

paper · pdf · doi:10.48550/arxiv.math/0410224

arxiv created 2004/10/08 · arxiv updated 2009/12/01

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.

Related

• Homotopical and Higher Categorical Structures in Algebraic Geometry
• Algebra and logic. Some problems
• Basic Set Theory and Algebra: Hints on Representation, Topology, Geometry, Analysis
• An Introduction to Categorical Proof Theory
• Theorem Proving and Algebra