« Tel nombre est premier », « tels graphes sont isomorphes », « telle classification est complète », etc. Traditionnellement, en mathématiques, la certitude concernant de telles affirmations formelles ne peut résulter que d'une démonstration. La pratique, cependant, semble remettre en question certaines des idées communément admises en la matière. L'informatique n'introduit-elle pas une nouvelle conception de la vérité mathématique, conception incompatible avec celle, défendue depuis plus de deux millénaires, qui se fonde sur la seule intelligence humaine ?
Pour aborder ces questions, détaillons deux situations où clairement l'ordinateur joue un rôle central dans l'étude d'énoncés mathématiques. Dans chaque cas, nous verrons que l'idée de la démonstration hilbertienne – des axiomes et des règles de raisonnement, codifiés une fois pour toutes, fixant ce que l'on considère comme vrai – est remise en cause comme seul moyen d'atteindre la certitude mathématique.
La cryptographie a fréquemment besoin de grands nombres premiers (de cent chiffres décimaux et plus) et aucune méthode sûre ne permet auj […]
