Ceci est une discussion informelle de la façon dont le problème de la construction des variétés algébriques avec diverses comportements topologiques, motive la recherche des méthodes formelles dans l'écriture des mathématiques vérifée sur machine. Aussi incluse est une discussion brève de mes travaux sur la formalisation de la théorie des catégories dans un environnement “ZFC” en utilisant l'assistant de preuves Coq.