Formalized proof, computation, and the construction problem in algebraic   geometry
  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. 
Carlos T. Simpson (JAD)