Topos et Démonstrations

Dans cet exposé fait à Luminy en mai 2007, est essentiellement discutée la notion d'indiscernabilité des preuves. Des arguments sont donnés en faveur de ce principe, aussi bien provenant de l'analyse du comportement des mathématiciens, que d'une modélisation des mathématiques dans les topos. On y parle également du système de types de Martin-Löf et de ses rapports avec le théorème de Diaconescu. Le caractère partiellement constructif de l'axiome du choix est aussi discuté.