La vérité en mathématiques et en informatique: la perte des certitudes...

L'informatique a mécanisé de nombreuses tâches, mais elle pose un défi majeur : garantir que les programmes font ce qu'ils sont censés faire. Un résultat fondamental de l'informatique théorique établit qu'il est impossible de prédire à l'avance si un programme quelconque va terminer ou entrer dans une boucle infinie — c'est l'indécidabilité du problème de l'arrêt, une limite incontournable enseignée dans les masters d'informatique.

Pour assurer la correction des programmes face à un nombre infini de configurations possibles, les informaticiens s'appuient sur des preuves mathématiques rigoureuses. La démonstration par récurrence, héritée des mathématiques grecques, permet d'établir des propriétés valables pour tous les entiers naturels. Cela a conduit à formaliser la notion de preuve elle-même grâce à la logique mathématique et à la théorie de la démonstration.

Cependant, deux problèmes majeurs subsistent : les démonstrations humaines, notamment les plus longues, risquent de contenir des erreurs non détectées (comme ce fut le cas pour certains problèmes de Hilbert). C'est pourquoi les informaticiens modernes ont développé des outils pour vérifier mécaniquement les preuves formelles par ordinateur, ouvrant une nouvelle approche de la validation mathématique.