Preuve assistée par ordinateur

Une preuve assistée par ordinateur est une preuve mathématique qui a été au moins partiellement générée par ordinateur .

La plupart des démonstrations assistées par ordinateur réalisées jusqu'à présent sont des implémentations de démonstrations par exhaustion de théorèmes mathématiques de grande envergure. Le principe consiste à utiliser un programme informatique pour effectuer des calculs complexes et à démontrer que le résultat de ces calculs implique le théorème donné. En 1976, le théorème des quatre couleurs fut le premier théorème majeur à être vérifié à l'aide d'un programme informatique .

Des efforts ont également été déployés dans le domaine de la recherche en intelligence artificielle pour créer de nouvelles démonstrations plus concises et explicites de théorèmes mathématiques, en partant de zéro et en utilisant des techniques de raisonnement automatisé telles que la recherche heuristique . Ces démonstrateurs de théorèmes automatisés ont démontré de nombreux résultats nouveaux et trouvé de nouvelles démonstrations pour des théorèmes connus. De plus, des assistants de démonstration interactifs permettent aux mathématiciens d'élaborer des démonstrations lisibles par l'humain, tout en garantissant formellement leur exactitude. Comme ces démonstrations sont généralement vérifiables par un humain (bien que cela puisse s'avérer difficile, comme c'est le cas pour la démonstration de la conjecture de Robbins ), elles ne présentent pas les mêmes implications controversées que les démonstrations par exhaustion assistées par ordinateur.

Une méthode d'utilisation de l'informatique dans les démonstrations mathématiques repose sur les calculs numériques validés ou rigoureux. Il s'agit d'effectuer des calculs numériques tout en respectant la rigueur mathématique. On utilise l'arithmétique ensembliste et le principe d'inclusion pour garantir que la sortie ensembliste d'un programme numérique englobe la solution du problème mathématique initial. Ceci est réalisé en contrôlant, en encadrant et en propageant les erreurs d'arrondi et de troncature, par exemple à l'aide de l'arithmétique d'intervalles . Plus précisément, on réduit le calcul à une séquence d'opérations élémentaires . Sur un ordinateur, le résultat de chaque opération élémentaire est arrondi à la précision de l'ordinateur. Cependant, on peut construire un intervalle défini par des bornes supérieure et inférieure du résultat d'une opération élémentaire. On remplace ensuite les nombres par des intervalles et on effectue des opérations élémentaires entre ces intervalles de nombres représentables.

Les démonstrations assistées par ordinateur font l'objet de controverses dans le monde mathématique, Thomas Tymoczko ayant été le premier à formuler des objections. Les partisans de ses arguments estiment que les démonstrations assistées par ordinateur, souvent longues, ne constituent pas, en un sens, de « véritables » démonstrations mathématiques , car elles impliquent un si grand nombre d'étapes logiques qu'elles sont pratiquement impossibles à vérifier par l'être humain. Ils considèrent également que les mathématiciens sont en réalité invités à remplacer le raisonnement logique à partir d'axiomes supposés par une confiance aveugle en un processus de calcul empirique, potentiellement affecté par des erreurs dans le programme informatique, ainsi que par des défauts de l'environnement d'exécution et du matériel.

D'autres mathématiciens estiment que les démonstrations assistées par ordinateur, même longues, devraient être considérées comme des calculs plutôt que comme des démonstrations : l'algorithme de démonstration lui-même devrait être validé, afin que son utilisation puisse alors être considérée comme une simple « vérification ». Les arguments selon lesquels les démonstrations assistées par ordinateur sont sujettes à des erreurs dans leurs programmes sources, leurs compilateurs et leur matériel peuvent être levés en fournissant une preuve formelle de la correction du programme informatique (une approche qui a été appliquée avec succès au théorème des quatre couleurs en 2005), ainsi qu'en reproduisant le résultat à l'aide de différents langages de programmation, de différents compilateurs et de différents matériels informatiques.

Une autre méthode pour vérifier les démonstrations assistées par ordinateur consiste à générer leurs étapes de raisonnement sous une forme lisible par machine , puis à utiliser un programme de vérification de démonstrations pour en démontrer l'exactitude. La validation d'une démonstration étant bien plus simple que sa recherche, le programme de vérification est plus simple que le programme d'assistance initial, et il est donc plus aisé de s'assurer de son exactitude. Toutefois, cette approche, qui consiste à utiliser un programme informatique pour prouver l'exactitude du résultat d'un autre programme, ne séduit pas les sceptiques à l'égard des démonstrations informatiques. Ils y voient une complexité supplémentaire qui ne répond pas au besoin perçu de compréhension humaine.

Un autre argument contre les démonstrations assistées par ordinateur est leur manque d'élégance mathématique : elles n'apporteraient ni idées nouvelles ni concepts utiles. En réalité, cet argument pourrait être avancé contre toute démonstration par exhaustion assez longue.

Une autre question philosophique soulevée par les démonstrations assistées par ordinateur est celle de savoir si elles transforment les mathématiques en une science quasi empirique , où la méthode scientifique prendrait le pas sur l'application du raisonnement pur dans le domaine des concepts mathématiques abstraits. Ceci est directement lié au débat qui anime les mathématiques quant à savoir si elles reposent sur des idées ou si elles ne sont « que » de simples exercices de manipulation de symboles formels. Cela soulève également la question de savoir si, selon la conception platonicienne , tous les objets mathématiques possibles « existent déjà » d'une certaine manière, les mathématiques assistées par ordinateur relèvent d'une science observationnelle comme l'astronomie, plutôt que d'une science expérimentale comme la physique ou la chimie. Cette controverse au sein des mathématiques se déroule en même temps que des interrogations émergent dans la communauté des physiciens quant à la question de savoir si la physique théorique du XXIe siècle ne devient pas trop mathématique et ne s'éloigne pas de ses fondements expérimentaux.

Le domaine émergent des mathématiques expérimentales aborde ce débat de front en privilégiant les expériences numériques comme principal outil d'exploration mathématique.

L'inclusion dans cette liste n'implique pas l'existence d'une preuve formelle vérifiée par ordinateur, mais plutôt l'intervention d'un programme informatique. Consultez les articles principaux pour plus de détails.