Preuves trouvées par ordinateur

11

En 1996, un problème ouvert de longue date a été résolu par un ordinateur; à savoir que l' algèbre de Robbins et l'algèbre booléenne sont les mêmes. La preuve a été trouvée par un prouveur de théorème automatisé.

De plus, la preuve connue du théorème des quatre couleurs contient des composants générés par ordinateur.

Le but de cette question est d'énumérer les preuves qui sont (totalement ou partiellement) trouvées par ordinateur (que ce soit la seule preuve connue ou celle découverte pour la première fois).

soft-question big-list proofs automated-theorem-proving Mahdi Cheraghchi
la source
2
Certains groupes simples finis sporadiques (comme le groupe de Lyon ont d'abord été construits à l'aide d'un ordinateur, c'est-à-dire que leur preuve d'existence a été (partiellement) générée par ordinateur.
jp
La question est «La théorie de la complexité exporimentale» utilisée pour résoudre les problèmes ouverts est liée à celle-ci.
adrianN
À mon humble avis, vous devez distinguer plus soigneusement entre «trouvé» et «vérifié». La preuve de Gonthier et al. N'a certainement pas été trouvée par un ordinateur.
gallais
1
belle question mais hélas presque équivalente à où et comment les ordinateurs ont-ils aidé à prouver un thm
vzn
Également très similaire: un résultat inconnu auparavant a-t-il été prouvé par un prouveur de théorème automatisé? .
Petr Pudlák

Réponses:

12

Un autre exemple célèbre est la preuve de Hales de la conjecture de Kepler qui avait un très grand composant assisté par ordinateur.

De Wikipédia :

En août 1998, Hales a annoncé que la preuve était complète. À ce stade, il comprenait 250 pages de notes et 3 gigaoctets de programmes informatiques, de données et de résultats.

Huck Bennett
la source
10

Il s'agit plus d'une méta-réponse en ce sens qu'il s'agit d'une liste de listes.

  1. Les papiers de Doron Zeilberger . Il est mathématicien et son ordinateur est répertorié par le co-auteur Shalosh B. Ekhad sur tous les papiers où l'ordinateur a joué un rôle dans la dérivation des résultats.

  2. Oeuvre de Georges Gonthier . Il a conçu une preuve vérifiée par machine du théorème des quatre couleurs et a récemment travaillé sur le théorème de Feit-Thompson. Il a récemment terminé la formalisation du théorème des ordres impairs.

  3. Archive of Formal Proofs contient des preuves vérifiées avec Isabelle, et comprend des théorèmes de correction pour les algorithmes, le théorème de Gauss-Jordan, une théorie de l'ordre, une théorie des catégories et bien d'autres résultats classiques.

  4. Formalisation de 100 théorèmes , contient des preuves vérifiées par machine de certains théorèmes célèbres.

Vijay D
la source
1
Merci. Je dois préciser que ma question ne concerne pas les preuves vérifiées / validées par les ordinateurs après leur découverte, ni les résultats lorsqu'un ordinateur a joué un rôle qui les dérive (bien sûr, nous utilisons tous des ordinateurs dans nos recherches, mais finissons finalement avec une mathématique autonome preuve que l'on ne peut pas dire qu'elle a été "dérivée" par un ordinateur). Je recherche des conjectures dont les preuves ont été générées (en tout ou en partie) par un ordinateur.
Mahdi Cheraghchi