Vom Computer gefundene Beweise

11

1996 wurde ein seit langem offenes Problem von einem Computer gelöst; nämlich, dass Robbins Algebra und Boolesche Algebra gleich sind. Der Beweis wurde von einem automatisierten Theorembeweiser gefunden.

Darüber hinaus enthält der bekannte Beweis des Vierfarbensatzes computergenerierte Komponenten.

Ziel dieser Frage ist es, Beweise aufzulisten, die (vollständig oder teilweise) vom Computer gefunden wurden (unabhängig davon, ob es sich um den einzigen bekannten oder den zum ersten Mal entdeckten Beweis handelt ).

soft-question big-list proofs automated-theorem-proving MCH
quelle
2
Einige sporadisch endliche einfache Gruppen (wie die Lyoner Gruppe wurden zuerst unter Verwendung eines Computers konstruiert, dh ihr Existenznachweis wurde (teilweise) computergeneriert.
jp
Die Frage, ob "Exporimental Complexity Theory" zur Lösung offener Probleme verwendet wird, hängt mit dieser zusammen.
AdrianN
IMHO müssen Sie genauer zwischen "gefunden" und "geprüft" unterscheiden. Der Beweis von Gonthier et al. Wurde definitiv nicht von einem Computer gefunden.
Gallais
1
nette
frage,
Ebenfalls sehr ähnlich: Wurde ein bisher unbekanntes Ergebnis von einem automatisierten Theorembeweiser bewiesen? .
Petr Pudlák

Antworten:

12

Ein weiteres berühmtes Beispiel ist Hales 'Beweis für Keplers Vermutung, die eine sehr große computergestützte Komponente hatte.

Aus Wikipedia :

Im August 1998 gab Hales bekannt, dass der Beweis vollständig sei. Zu diesem Zeitpunkt bestand es aus 250 Seiten Notizen und 3 Gigabyte Computerprogrammen, Daten und Ergebnissen.

Huck Bennett
quelle
10

Dies ist eher eine Meta-Antwort, da es sich um eine Liste von Listen handelt.

  1. Die Papiere von Doron Zeilberger . Er ist Mathematiker und sein Computer ist beim Co-Autor Shalosh B. Ekhad auf allen Papieren aufgeführt, auf denen der Computer eine Rolle bei der Ableitung der Ergebnisse gespielt hat.

  2. Arbeit von Georges Gonthier . Er erstellte einen maschinengeprüften Beweis für den Vierfarbensatz und arbeitete kürzlich am Feit-Thompson-Satz. Kürzlich hat er die Formalisierung des Satzes der ungeraden Ordnung abgeschlossen.

  3. Das Archiv formaler Beweise enthält mit Isabelle überprüfte Beweise sowie Korrektheitssätze für Algorithmen, den Gauß-Jordan-Satz, einige Ordnungstheorien, Kategorietheorien und viele weitere klassische Ergebnisse.

  4. Die Formalisierung von 100 Theoremen enthält maschinengeprüfte Beweise einiger berühmter Theoreme.

Vijay D.
quelle
1
Vielen Dank. Ich sollte klarstellen, dass meine Frage weder Beweise betrifft, die von Computern nach ihrer Entdeckung verifiziert / validiert wurden, noch Ergebnisse, bei denen ein Computer eine Rolle bei der Ableitung gespielt hat (natürlich verwenden wir alle Computer in unserer Forschung, aber am Ende haben wir eine in sich geschlossene Mathematik Der Beweis, dass wir nicht sagen können, wurde von einem Computer "abgeleitet". Ich suche nach Vermutungen, deren Beweise (ganz oder teilweise) von einem Computer generiert wurden .
MCH