Wo und wie haben Computer geholfen, einen Satz zu beweisen?

Ziel dieser Frage ist es, Beispiele aus der theoretischen Informatik zu sammeln, bei denen der systematische Einsatz von Computern hilfreich war

1. beim Aufbau einer Vermutung, die zu einem Theorem führt,
2. eine Vermutung oder einen Beweisansatz fälschen,
3. Konstruktion / Überprüfung (von Teilen) eines Beweises.

Wenn Sie ein bestimmtes Beispiel haben, beschreiben Sie bitte, wie es gemacht wurde. Vielleicht hilft dies anderen dabei, Computer in ihrer täglichen Forschung effektiver zu nutzen (was in TCS derzeit noch eine recht ungewöhnliche Praxis zu sein scheint).

(Als Community-Wiki gekennzeichnet, da es keine "richtige" Antwort gibt.)

Ein sehr bekanntes Beispiel ist das Vier-Farben-Theorem , das ursprünglich durch eingehende Prüfung bewiesen wurde.

$n$

Es zeigte sich, dass das Minimum Weight Triangulation (MWT) -Problem NP-hart war und lange Zeit offen war. Dies wurde durch die Tatsache erschwert, dass Kantenlängen Quadratwurzeln beinhalten und die gewünschte Genauigkeit, die für die genaue Berechnung erforderlich war, nur schwer zu erreichen war.

Mulzer und Rote zeigten, dass MWT NP-hart war , und verwendeten dabei Computerunterstützung, um die Richtigkeit ihrer Geräte zu überprüfen. Soweit ich weiß, gibt es keinen alternativen Beweis.

Thomas Hales 'Beweis (seine Website, MathSciNet ) für die Kepler-Vermutung umfasste so viele Fallanalysen - und die Fälle wurden wiederum durch Computer verifiziert -, dass er sich entschied, einen formellen Beweis dafür zu versuchen. Sein Projekt dazu ist FlysPecK und er schätzt, dass es 20 Jahre dauern wird.

Forscher in Programmiersprachen verwenden regelmäßig computergestützte Beweise in ihrer Arbeit, obwohl ich nicht weiß, wie wichtig dies für ihren Forschungsprozess ist (es hindert sie jedoch sicherlich daran, Tonnen mühsamer Manipulationen aufschreiben zu müssen).

Doron Zeilberger hat einige Arbeiten auf dem Gebiet der computergenerierten Proofs ausgeführt. Insbesondere hat er ein Maple-Programm zum Nachweis geometrischer Identitäten und ein weiteres Programm zum Nachweis einer Klasse kombinatorischer Identitäten vorbereitet . Einige der Methoden sind im Buch A = B aufgeführt .

Computer wurden auch verwendet, um Obergrenzen für die Laufzeit von Backtracking-Programmen zu bestimmen, die NP-harte Probleme lösen, und um Gadgets zu konstruieren, die Unannäherungsergebnisse beweisen. Dieses und andere unterhaltsame Themen erwarten Sie in einem kurzen Aufsatz (Warnung, extreme Eigenwerbung voraus) mit dem Titel "Anwenden von Praxis auf Theorie". Siehe http://arxiv.org/abs/0811.1305

Angesichts dieser netten Liste sollte ich wohl das Papier aktualisieren!

Ein Gegenbeispiel zur Hirsch-Vermutung , die für die lineare Programmierung und die polyedrische Kombinatorik wichtig ist, wurde kürzlich von Francisco Santos vorgeschlagen. Die Computerverifikation wurde zuerst verwendet, um einige der für das Beispiel erforderlichen Eigenschaften zu ermitteln, obwohl später Argumente ohne die Unterstützung von Rechenleistung entdeckt wurden, vgl. Gil Kalais Blogpost oder das Paper über Arxiv .

Ich habe das hier nicht gesehen, aber ein automatisierter Theorembeweiser hat das seit langem offene Problem gelöst, ob Robbins-Algebren boolesch sind:

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

Dies ist insbesondere deshalb bemerkenswert, weil der Computer den gesamten Beweis entwickelt hat und das Problem seit mehreren Jahrzehnten offen ist.

Nicht ganz sicher, ob es als TCS qualifiziert ist, aber es ist wohl eng verwandt.

Der Karloff-Zwick-Algorithmus für MAX-3SAT erreicht die erwartete Leistung 7/8. Die Analyse stützt sich jedoch auf nicht nachgewiesene Ungleichungen des Kugelvolumens. Diese Ungleichungen wurden schließlich durch computergestützte Beweise in Zwicks anderer Veröffentlichung bestätigt .

Neben dem oben erwähnten Beweis von Hales für die Kepler-Vermutung werden auch der Beweis für die Honeycomb-Vermutung und der für die Dodekaeder-Vermutung rechnergestützt.

Sie können die Homepage von Shalosh B. Ekhad besuchen . Dieser Computer veröffentlicht seit einiger Zeit Artikel (in der Regel mit Co-Autoren).

Christian Urban verwendete den Isabelle-Beweisassistenten, um einen der Hauptsätze in seiner Doktorarbeit zu überprüfen, der eigentlich ein Theorem war [1]. Mit dem Assistenten mussten ein paar Änderungen vorgenommen werden, aber das Ergebnis war ziemlich zufriedenstellend.

In ähnlicher Weise entdeckten Urban und Narboux auch Fehler in einem Stift- und Papiernachweis für Crarys Vollständigkeitsnachweis für die Äquivalenzprüfung.

Meikle und Fleuriot formalisierten Hilberts Grundlagen in Isabelle und zeigten, dass er sich entgegen Hilberts Behauptungen immer noch auf seine Intutition stützte, Geometrie auf axiomatische Weise zu formalisieren (IIRC: Es gab Lücken in seinem Beweis, die von Hilberts Annahme von Dingen über Diagramme abgeleitet wurden). [3] .

[1]: Erneutes Aufrufen von Cut-Elimination: Ein schwieriger Beweis ist wirklich ein Beweis

[2]: Formalisierung in Nominal Isabelle Crarys Vollständigkeitsnachweis für die Äquivalenzprüfung

[3]: Formalisierung von Hilberts Grundlagen in Isabelle / Isar

Die Ergebnisse in " Die Geometrie binärer Suchbäume" von Demaine, Harmon, Iacono, Kane und Patraşcu wurden mit Hilfe von Software entwickelt, um verschiedene Ladeschemata zu testen und optimale Asses für kleine Zugriffssequenzen zu erstellen. (Und ja, "Esel" ist der richtige Begriff.)

N. Shankar überprüfte (vollständig und mechanisch) Godels Beweis für den Unvollständigkeitssatz und den Church-Rosser-Satz unter Verwendung des Boyer-Moore-Satzbeweises. Es gibt ein Buch, das beschreibt, wie es gemacht wurde.

Die Formel für den Bailey-Borwein-Plouffe-Algorithmus zur Berechnung des n-ten Bits von Pi ohne Berechnung eines der höherwertigen Bits wurde laut Simon Plouffe unter Verwendung von Computersystemen entdeckt.

Es gibt zahlreiche Beispiele für die Durchschnittsanalyse von Algorithmen. Vielleicht sind einige der frühesten die Computerexperimente, die zu der Veröffentlichung "Einige unerwartet erwartete Verhaltensergebnisse für das Verpacken von Behältern" von Bentley, Johnson, Leighton, McGeoch und McGeoch in STOC 1984 führten.