Seminars

Henri Lombardi (Université de Besançon)

Title: Évaluation dynamique et preuves constructives

Abstract:
Le système D5 a montré comment utiliser l'évaluation paresseuse
pour travailler dans la cloture algébrique d'un corps même quand cette dernière
n'a pas d'existence, au sens constructif du mot exister.
Cette merveille (le système D5) a donné lieu
à l'idée générale de remplacer les objets trop abstraits (sans existence effective)
des mathématiques cantoriennes par leurs approximations finies, et d'obtenir de
cette manière des preuves constructives pour l'existence d'objets concrets quand ceux-ci
semblent résulter de tours de magie.
Il s'agit ici d'une réalisation partielle du programme de Hilbert
pour l'algèbre abstraite, et plus précisément d'une réalisation du
programme de Poincaré.
Nous illustrerons ces idées sur quelques exemples.