{'fraction_non_alphanumeric': 0.02188006482982172, 'fraction_numerical': 0.0032414910858995136, 'mean_word_length': 5.144278606965174, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
FORMALIZED PROOF, COMPUTATION, AND THE CONSTRUCTION PROBLEM IN ALGEBRAIC GEOMETRY

It has become a classical technique to turn to theoretical computer science to provide computational tools for algebraic geometry. A more recent transformation is that now we also get logical tools, and these too should be useful in the study of algebraic varieties. The purpose of this note is to consider a very small part of this picture, and try to motivate the study of computer theorem-proving techniques by looking at how they might be relevant to a particular class of problems in algebraic geometry. This is only an informal discussion, based more on questions and possible research directions than on actual results. This note amplifies the themes discussed in my talk at the “Arithmetic and Differential Galois Groups” conference (March 2004, Luminy), although many specific points in the discussion were only finished more recently. I would like to thank: André Hirschowitz and Marco Maggesi, for their invaluable insights about computer-formalized mathematics as it relates to algebraic geometry and category theory; and Benjamin Werner, M. S. Narasimhan, Alain Connes, Andy Magid and Ehud Hrushowski for their remarks as explained below.