Où et comment les ordinateurs ont-ils aidé à prouver un théorème?

Le but de cette question est de recueillir des exemples d'informatique théorique où l'utilisation systématique des ordinateurs était utile.

1. dans la construction d'une conjecture qui mène à un théorème,
2. falsifier une conjecture ou une approche par preuve,
3. construire / vérifier (des parties de) une preuve.

Si vous avez un exemple spécifique, veuillez décrire comment cela a été réalisé. Cela aidera peut-être d'autres utilisateurs à utiliser l'ordinateur plus efficacement dans leurs recherches quotidiennes (ce qui semble encore être une pratique assez rare dans le SDC à ce jour).

(Signalé en tant que wiki de communauté, car il n'y a pas de réponse "correcte" unique.)

Un exemple très connu est le théorème des quatre couleurs , prouvé à l'origine par un contrôle exhaustif.

Fixe points dans le plan. Soit T une triangulation (c’est-à-dire un graphe rectiligne plan avec les points sous forme de sommets entièrement triangulés), et la pondération de la triangulation correspond à la somme des longueurs des arêtes.$n$

Démontrer que le problème de la triangulation en poids minimum (PTM) était NP-difficile était un problème ouvert de longue date, rendu difficile par le fait que les longueurs des arêtes impliquent des racines carrées, et la précision souhaitée pour les calculer avec précision était difficile à relier.

Mulzer et Rote ont montré que MWT était NP-difficile et ont utilisé une assistance informatique pour vérifier l'exactitude de leurs gadgets. Pour autant que je sache, il n'y a pas de preuve alternative.

La preuve de Thomas Hales (son site, MathSciNet ) de la conjecture de Kepler impliquait tellement d’analyses de cas - et les cas ont été ensuite vérifiés par ordinateur - qu’il a décidé de tenter une preuve formelle à ce sujet. FlysPecK est son projet et il estime que 20 ans de travail seront nécessaires.

Les chercheurs en langages de programmation utilisent régulièrement des démonstrations assistées par ordinateur dans leurs travaux, même si je ne sais pas à quel point cela est essentiel pour leur processus de recherche (cela les empêche certainement de devoir écrire des tonnes de manipulations fastidieuses).

Doron Zeilberger a effectué des travaux dans le domaine des épreuves générées par ordinateur. Il a notamment préparé un programme Maple pour prouver les identités géométriques et un autre programme pour prouver une classe d' identités combinatoires . Certaines des méthodes sont mentionnées dans le livre A = B .

Les ordinateurs ont également été utilisés pour déterminer la limite supérieure des temps d'exécution des programmes de retour en arrière résolvant les problèmes difficiles à résoudre, et pour créer des gadgets permettant de prouver des résultats inapproximables. Ceci et d'autres sujets amusants vous attendent dans un court essai (mise en garde, auto-promotion extrême à venir) intitulé "Application de la pratique à la théorie". Voir http://arxiv.org/abs/0811.1305

Compte tenu de cette belle liste, il semble que je devrais mettre à jour le papier!

Francisco Santos a récemment proposé un contre-exemple de la conjecture de Hirsch , important pour la programmation linéaire et la combinatoire polyhédrale. La vérification sur ordinateur a d'abord été utilisée pour établir certaines des propriétés requises de l'exemple, bien que des arguments sans l'aide de la puissance de calcul aient été découverts plus tard, cf. Le billet de blog de Gil Kalai ou l' article sur arxiv .

Je n'ai pas vu cela mentionné ici, mais un prouveur de théorèmes automatisé a résolu le problème ouvert de savoir si les algèbres de Robbins sont booléennes:

http://www.cs.unm.edu/~mccune/papers/robbins/

Cela est d'autant plus remarquable que l'ordinateur a développé toute la preuve et que le problème était ouvert depuis plusieurs décennies.

Pas tout à fait sûr s'il est qualifié de TCS, mais on peut dire qu'il est étroitement lié.

L' algorithme Karloff – Zwick pour MAX-3SAT atteint les performances attendues 7/8. Cependant, l'analyse repose sur des inégalités de volume sphériques non prouvées. Ces inégalités ont finalement été confirmées par des preuves assistées par ordinateur dans un autre document de Zwick .

Outre la preuve de Hales à la conjecture de Kepler, comme mentionné ci-dessus, la preuve à la conjecture Honeycomb et celle à la conjecture Dodécaèdre sont également assistées par ordinateur.

Vous pouvez consulter la page d' accueil de Shalosh B. Ekhad . Cet ordinateur publie des articles depuis un certain temps (généralement avec des coauteurs).

Christian Urban a utilisé l'assistant de preuves d'Isabelle pour vérifier qu'un des théorèmes principaux de sa thèse était en réalité un théorème [1]. À l’aide de l’assistant, quelques modifications ont dû être apportées, mais le résultat est plutôt valable.

De même, Urban et Narboux ont également découvert des erreurs dans un stylo et une preuve papier de la preuve de complétude de Crary pour la vérification de l'équivalence.

Meikle et Fleuriot ont officialisé le Grundlagen de Hilbert dans Isabelle et ont démontré que, contrairement à ce que prétend Hilbert, il comptait toujours sur son intuition pour formaliser la géométrie de manière axiomatique (IIRC présentait des trous dans sa preuve, car Hilbert supposait des choses comme des diagrammes) [3] .

[1]: Revisiter Coupe-Élimination: Une preuve difficile est vraiment une preuve

[2]: Mise en forme de la preuve de complétude de Isabelle Crary pour le contrôle d'équivalence

[3]: Formaliser le Grundlagen de Hilbert dans Isabelle / Isar

Les résultats de " La géométrie des arbres de recherche binaires " de Demaine, Harmon, Iacono, Kane et Patraşcu ont été développés à l'aide d'un logiciel permettant de tester divers systèmes de charge et de construire des culs optimaux pour de petites séquences d'accès. (Et oui, "ânes" est le terme correct.)

N. Shankar a vérifié (complètement et mécaniquement) la preuve de Godel du théorème de l'incomplétude et du théorème de Church-Rosser à l'aide du prouveur de théorème de Boyer-Moore. Il y a un livre décrivant comment cela a été fait.

La formule de l' algorithme Bailey-Borwein-Plouffe pour calculer le nième bit de Pi sans calculer aucun des bits les plus significatifs a été découverte, selon Simon Plouffe , à l'aide de systèmes informatiques.

L'analyse des cas moyens d'algorithmes comporte de nombreux exemples. Parmi les premières expériences informatiques, celles de Bentley, Johnson, Leighton, McGeoch et McGeoch, publiées dans le STOC 1984, "Quelques résultats inattendus en matière de comportement des emballages de bacs".