La théorie des Ensembles est encore aujourd'hui considérée comme la fondation la plus complète de l'ensemble des disciplines mathématiques.
Cependant, certains développements de la fin du siècle dernier (ayant leurs origines dans la fin du XIXè siècle!) permettent de donner d'autres fondations, plus propices aux mathématiques formalisées sur ordinateur ; c'est la théorie des Types.
Nous donnerons une esquisse de cette théorie, et un exemple de formalisation informatique de mathématiques connues de tous.