Dans les années 1920, le grand mathématiciens allemand a formulé un important programme de recherches relatif aux fondements des mathématiques. Destiné notamment à s'assurer, après l'épisode des paradoxes de la théorie des ensembles, qu'aucune contradiction n'était capable de menacer les mathématiques, ce programme est à l'origine lointaine d'une bonne part de la logique mathématique contemporaine (théorie de la démonstration). L'exposé présentera le programme, la manière dont il a été affecté par les résultats d'incomplétude de Gödel (1931) et essaiera d'évaluer ce qu'il a encore d'actuel aujourd'hui.