 Séminaires et Congrès - 13 - pages 367-387 | |
|
| | |
Groupes de Galois arithmétiques et différentiels. Actes du colloque du CIRM (Luminy, 8-13 Mars 2004)
Daniel Bertrand - Pierre Dèbes (Éd.)
Séminaires et Congrès 13 (2006), xxii+391 pages
Formalized proof, computation, and the construction problem in algebraic geometry
Carlos Simpson
Séminaires et Congrès 13 (2006), 367-387
Download :
PDF file
Résumé :
Les preuves formalisées, le calcul, et le problème de la construction en géométrie algébrique
Ceci est une discussion informelle de la façon dont le problème de la construction des variétés algébriques avec diverses comportements topologiques, motive la recherche des méthodes formelles dans l'écriture des mathématiques vérifée sur machine. Aussi incluse est une discussion brève de mes travaux sur la formalisation de la théorie des catégories dans un environnement ``ZFC'' en utilisant l'assistant de preuves Coq.
Mots clefs : Connexion, groupe fondamental, représentation, catégorie, preuve formelle, variété algébrique, inégalité de Bogomolov-Gieseker, limite, catégorie des foncteurs
Abstract:
This is an informal discussion of how the construction problem in algebraic geometry, that is the problem of constructing algebraic varieties with various topological behaviors, motivates the search for methods of doing mathematics in a formal, machine-checked way. I also include a brief discussion of some of my work on the formalization of category theory within a ZFC-like environment in the Coq proof assistant.
Key words: Connection, fundamental group, representation, category, formalized proof, algebraic variety, Bogomolov-Gieseker inequality, limit, functor category
Class. math. : 03B35, 32J25, 18A25