Abstract FR:

Cette thèse s’intéresse à quelques aspects de la formalisation des mathématiques, et plus spécialement des mathématiques classiques, dans le calcul des constructions inductives (CCI), le système logique implanté dans le logiciel d’aide à la démonstration Coq. Trois principaux travaux ont été réalisés. La première partie fait état d’un travail de formalisation d’algèbre, topologie et théorie des faisceaux en vue de la définition des schémas affines, ainsi que de la spécification du lemme d’Horace. La deuxième partie s’intéresse aux types quotients, on montre qu’il ne peut y avoir dans le CCI de notion catégorique de type quotient qui soit aussi expressive que les ensembles quotients en mathématiques classiques. Enfin, on montre en troisième partie l’incohérence dans le CCI de l’ajout simultané de l’axiome du choix et du tiers exclu sous forme propositionnelle.