Lässige Touren rund um Beweise

Heute hat Ryan Williams einen Artikel über das arXiv veröffentlicht (der zuvor in den SIGACT News veröffentlicht wurde), der eine weniger technische Version seiner jüngsten ACC- Technik für untere Schranken enthält.

Meine Frage bezieht sich nicht auf die Technik selbst (natürlich verdient großes Lob), sondern auf den Stil des Papiers. In der Zusammenfassung schreibt er:

Der Beweis wird aus der Perspektive von jemandem beschrieben, der versucht, ihn zu entdecken.

Genial! Im Abschnitt Hintergrund fügt er hinzu:

Dieser Artikel ist eine Diskussion darüber, wie man den Beweis findet - eine beiläufige Tour um ihn herum. Es werden nicht alle Details angegeben, aber Sie werden sehen, woher alle Teile stammen und wie sie zusammenpassen. Der Weg wird mit meinen eigenen voreingenommenen Intuitionen über die Komplexitätstheorie übersät sein - was ich denke, sollte und sollte nicht wahr sein und warum. Ein Großteil dieser Intuition ist möglicherweise falsch. Ich kann jedoch sagen, dass es mich mindestens einmal in eine produktive Richtung geführt hat.

Das ist unglaublich und es ist das erste Mal, dass ich es gesehen habe. Ich habe mich immer gefragt, warum Autoren von Papier nicht schreiben, wie sie zum Beweis gekommen sind, einschließlich der fehlgeschlagenen Ansätze, die sie versucht haben, bevor sie zu dem Weg gekommen sind, der zur Lösung geführt hat. Als ich Ryans Artikel auf dem arXiv sah, fühlte ich mich sehr motiviert, ihn zu lesen. Ich halte es aus dieser Sicht für ein revolutionäres Papier. Meistens können Sie mit einem Papier nur die Richtigkeit überprüfen.

Die Frage ist folgende:

• Kennen Sie andere Veröffentlichungen in TCS, in denen ein Durchbruch eher in einer "Gelegenheitsreise" als in einer Reihe technischer Lemmata dargestellt wird?

Ich spreche von Veröffentlichungen in Zeitschriften, nicht von Blogposts oder technischen Berichten.

Außerdem habe ich es als große Liste markiert , mit der Hoffnung, dass es tatsächlich so sein wird.

Es gibt eine Veröffentlichung (2001) ähnlichen Stils von Lov Grover, die den Weg zu seinem bahnbrechenden Quantensuchalgorithmus (1996) beschreibt.

Tim Gowers ist ein Fan dieser Art von Dingen. Siehe insbesondere seine Darstellung der Annäherungsmethode von Rasborow .

In seiner Einleitung bezieht sich Gowers auf meinen Expository-Artikel über das Forcen , der ein (nicht ganz erfolgreicher) Versuch ist, dasselbe für das Forcen zu tun. Forcen wird normalerweise als eine Technik in der Logik- und Mengenlehre angesehen, hat aber gelegentlich Eingang in das TCS gefunden. Es taucht in der Untersuchung der Komplexität von beschränkten Arithmetik- und Satzbeweisen auf (Krajíček und Takeuti sind zwei Forscher, die diesen Zusammenhang verfolgt haben), und das Konzept eines generischen Orakels ist mit dem Konzept eines generischen Filters verwandt.

(Dies begann als Kommentar und wurde viel zu lange).

Sie können William Thurstons Artikel über Beweis und Fortschritt in der Mathematik genießen .

Mathematik hat in gewissem Sinne eine gemeinsame Sprache: eine Sprache der Symbole, technischen Definitionen, Berechnungen und Logik. Diese Sprache vermittelt effizient einige, aber nicht alle Modi des mathematischen Denkens. Mathematiker lernen, bestimmte Dinge fast unbewusst von einem mentalen Modus in den anderen zu übersetzen, so dass einige Aussagen schnell klar werden. [...]

Menschen, die mit der Vorgehensweise in einem Unterfeld vertraut sind, erkennen verschiedene Muster von Aussagen oder Formeln als Redewendungen oder Umschreibungen für bestimmte Konzepte oder mentale Bilder. Aber für Leute, die noch nicht mit den gleichen Mustern vertraut sind, sind sie nicht sehr aufschlussreich. Sie sind oft sogar irreführend. Die Sprache lebt nur für diejenigen, die sie benutzen. [...]

Wir Mathematiker müssen uns viel mehr anstrengen, um mathematische Ideen zu kommunizieren. Um dies zu erreichen, müssen wir viel mehr darauf achten, nicht nur unsere Definitionen, Theoreme und Beweise, sondern auch unsere Denkweisen zu kommunizieren. Wir müssen den Wert unterschiedlicher Denkweisen über dieselbe mathematische Struktur einschätzen. Wir müssen uns viel mehr darauf konzentrieren, die grundlegende mentale Infrastruktur der Mathematik zu verstehen und zu erklären - und folglich weniger auf die neuesten Ergebnisse. Dies beinhaltet die Entwicklung einer mathematischen Sprache, die effektiv ist, um Menschen, die sie noch nicht kennen, Ideen zu vermitteln.

In Bezug auf die ursprüngliche Frage gibt es Artikel, die keine Ideen im DTP-Format (Definition-Theorem-Proof) präsentieren. Timothy Chow hat einige Papiere, die sich auf die Vermittlung von Ideen konzentrieren (obwohl es sich nicht um die ersten (oder zweiten) Papiere zum Thema / Ergebnis handelt).

1. Sie hätten Spektralsequenzen erfinden können , Timothy Chow, Notices of the AMS
2. Timothy Chow ist auf der Suche nach Dummköpfen

Ein möglicher Grund für die Verbreitung des DTP-Formats ist, dass wir alle nur von Büchern und Zeitungen daran gewöhnt sind. Rezensenten (und Leser) finden manchmal nicht standardmäßigen Schreibstil ablenkend. Ein Mittelweg sind Papiere, die den Leser sanft in ein Ergebnis zerlegen. Es gibt Artikel, die einen speziellen Fall oder ein einfaches Problem darstellen, das die allgemeine Idee veranschaulicht.

1. Die topologische Struktur der asynchronen Berechenbarkeit , Maurice Herlihy und Nir Shavit. Der Artikel enthält viele Abbildungen und demonstriert die allgemeine Idee für ein einfaches Protokoll, bevor der Hauptsatz angewendet wird, um einige offene Probleme zu lösen.
2. $p$

Ohne die Erwähnung der Arbeit von Jean-Yves Girard wäre keine Diskussion über eine nicht standardmäßige Präsentation bemerkenswerter Ideen vollständig . Einzigartig ist wahrscheinlich das beste Wort, um es zu beschreiben (ohne diplomatisch oder sarkastisch zu sein). Aus dem Papier Linear Logic .

Die philosophische Exegese von Heytings Regeln lässt in der Tat sehr wenig Raum für eine weitere Diskussion des intuitionistischen Kalküls; aber hat jemand jemals ernsthaft versucht? Tatsächlich kann die lineare Logik, die eine klare und klare Erweiterung der üblichen Logik darstellt, durch eine übersichtlichere Analyse der Semantik von Beweisen erreicht werden (nicht sehr weit vom Ansatz der Informatik entfernt und daher in den nächsten Abschnitt verwiesen) oder durch bestimmte mehr oder weniger unmittelbare Überlegungen zur Folgerechnung. Diese Überlegungen sind von unmittelbarer geometrischer Bedeutung, aber um sie zu verstehen, muss man die Absichten vergessen, sich mit einem chinesischen Führer daran zu erinnern, dass nicht die Farbe der Katze von Bedeutung ist, sondern die Tatsache, dass sie Mäuse fängt.

Später:

Es gibt immer noch Leute, die sagen, dass man für die Herstellung von Informatik im Wesentlichen einen Lötkolben braucht. Diese Meinung wird von Logikern geteilt, die die Informatik verachten, und von Ingenieuren, die Theoretiker verachten. In den letzten Jahren wurde jedoch die Notwendigkeit einer logischen Erforschung der Programmierung immer deutlicher, und die Verknüpfung von Logik und Informatik scheint irreversibel. [...]
In gewisser Weise spielt die Logik dieselbe Rolle wie die Geometrie in der Physik: Der geometrische Rahmen legt bestimmte Erhaltungsergebnisse fest, zum Beispiel die Stokes-Formel. Die Symmetrien der Logik drücken vermutlich eine tiefe Bewahrung von Informationen in noch nicht richtig konzipierter Form aus.

Vielleicht nehmen die Autoren diese fehlgeschlagenen Versuche und die Geschichte der Forschung aufgrund der von Redakteuren und PC-Mitgliedern auferlegten Einschränkungen nicht in ihre veröffentlichten Arbeiten auf. Ich denke, es ist sehr ungewöhnlich für eine Zeitschrift (und wahrscheinlich noch ungewöhnlicher für eine Konferenz), ein Papier anzunehmen, in dem der Hauptteil davon gescheiterten Versuchen gewidmet ist. In den meisten Fällen werden Autoren oder Experten auf diesem Gebiet die Geschichte und die fehlgeschlagenen Versuche erklären (und viele sprechen in Workshops darüber).

Ich habe mehrere Autoren gesehen, die erklärt haben, woher die Ideen in ihren Papieren kamen. Als Beispiel erklärt Girard in seiner Arbeit, dass die Idee für die lineare Logik aus dem Versuch stammt, eine Denotationssemantik für das intuitionistische ODER zu finden. Informationen dieser Art finden Sie auch in Monografien und Biografien berühmter Forscher sowie in Bänden, die ihnen gewidmet sind ( Halmos 'Autobiografie und neuere "Kreiseliana: Über und um Georg Kreisel ", herausgegeben von Odifreddi). Es gibt auch Bände und Artikel einige Komplexitätstheoretiker gewidmet). Hoffentlich werden mehr Leute das tun, was Ryan getan hat, und den Prozess systematisch erklären und die Geschichte erzählen.

ps: Sie können sich dies als mündliche Überlieferung der Forschung vorstellen :) (etwas ähnlich der mündlichen Tora, die nicht aufgeschrieben werden durfte ).

Es gibt ein veröffentlichtes Papier von Laszlo Babai (1990) in Form einer Fabel über Arthur und Merlin die dramatische Abfolge der Ereignisse beschreiben , die Gemeinschaft im Jahr 1989 auf den IP = PSPACE Ergebnis führen, das nur ein Jahr früher sehr viel war unglaublich.