Das lebendige Theorem (German Edition)

Nächte verbracht. Genieße doch die Glühwürmchen, ohne dir Fragen zu stellen.
    Sieh mal an, wer geht hier auch noch so spät spazieren? Ich erkenne diese Silhouette wieder … Na, so was! Wladimir Wojewodski, einer der brillantesten russischen Mathematiker seiner Generation, Fields-Medaille 2002, einer der geistigen Erben von Grothendieck. Das ist die Art von unguter Begegnung, die man spät am Abend in Princeton erlebt.
    Wojewodski geht ebenfalls spazieren. Gehen, einfach nur gehen, um Luft zu schnappen, ohne bestimmtes Ziel, wie der Fußgänger von Ray Bradbury.
    Wir beginnen ein Gespräch. Man kann sich nur schwer jemanden vorstellen, der im Verhältnis zu mir eine unterschiedlichere Mathematik betreibt als Wojewodski. Ich verstehe kein einziges Wort von seinen Forschungen, und das Umgekehrte gilt wahrscheinlich ebenso. Aber anstatt zu versuchen, mir von seinen Arbeiten zu erzählen, spricht er von seinen Träumen, von einem Thema, das ihn begeistert und in das er sich voll und ganz versenken will, das der Expertensprachen und automatischen Beweise.

Wladimir Wojewodski
    Er spricht über das berühmte Vierfarben-Problem, von seinem umstrittenen Beweis, der aufgrund von Computerprogrammen unmenschlich geworden ist und vor kurzem durch Arbeiten französischer Forscher am INRIA mit Hilfe der Expertensprache Coq auf den Kopf gestellt wurde.
    Wladimir meint, dass in nicht allzu ferner Zukunft die Informatikprogramme lange und komplexe Argumente überprüfen könnten. Er sagt, dass das sogar in Frankreich bei berühmten Resultaten schon in der Experimentierphase ist. Zu Beginn bin ich zwar skeptisch, aber die Person, die ich vor mir habe, ist kein Schwärmer, sondern ein Wissenschaftler höchsten Ranges. Ich muss das also ernst nehmen.
    Ich habe mich mit diesen Problemen nie beschäftigt und nur ganz wenig Erfahrung mit Algorithmen. Heiratsalgorithmen ( bipartite matching ), Simplexalgorithmen, Versteigerungsalgorithmen spielen zwar eine wichtige Rolle für die numerische Simulation des optimalen Transports, für den ich Experte bin; aber das gehört zu einem ganz anderen Geist als das, wovon mir Wladimir erzählt. Dieser neue Bereich macht große Lust, es gibt so viele spannende Dinge zu erforschen.
    Blumen, Sprachen, vier Farben, Heirat … Alle Ingredienzen für ein schönes Chanson … Es sei denn, dass es vielleicht schon existiert?
    *
    Um 1850 färbt der Mathematiker Francis Guthrie die Landkarte der Grafschaften Englands, wobei er sorgfältig darauf achtete, dass zwei Grafschaften mit einer gemeinsamen Grenze verschieden gefärbt sein sollten. Wie viele Farbstifte muss er verwenden?
    Guthrie sieht ein, dass vier Farben ausreichen. Und sagt sich, dass vier vielleicht ausreichen, um jede beliebige Landkarte einzufärben, die allerdings Staaten zeigt, die nicht selbst wieder in getrennte Landesteile zerfallen.
    Drei Farben würden nicht ausreichen: Betrachten Sie die Landkarte von Südamerika, und schauen Sie sich Brasilien, Argentinien, Bolivien und Paraguay an. Jedes der vier Länder berührt die drei anderen, also brauchen Sie mindestens vier verschiedene Farben.
    Aber vier genügen, was Sie prüfen können, wenn Sie Ihre Lieblingslandkarte einfärben. Zumindest können Sie es an zahlreichen Beispielen überprüfen. Aber wie lässt sich zeigen, dass das für jede Landkarte gilt? Man kann sie nicht alle überprüfen, denn es gibt unendlich viele! Also braucht man eine logische Überlegung, und das ist nicht einfach.
    1879 glaubt Kempe, dieses Resultat bewiesen zu haben. Aber sein Beweis ist fehlerhaft und gestattet nur, zu zeigen, dass fünf Farben ausreichen.
    Gehen wir Schritt für Schritt vor. Für eine Landkarte von vier Ländern weiß man, wie es geht. Im Ausgang davon ist es leicht, den Beweis für fünf Länder zu führen. Dann für sechs. Lässt sich so weitermachen?
    Angenommen, man wüsste, wie man alle Landkarten mit 1000 Ländern einfärbt, und man wollte eine Landkarte mit 1001 Ländern in Angriff nehmen. Wie macht man das? Zu Beginn kann man beweisen, dass es unter diesen 1001 Ländern mindestens eines gibt, das wenig Grenzländer hat, sagen wir maximal 5. Wenn man sich auf dieses Land und seine Nachbarn konzentriert, ist das Einfärben leicht; und wenn man Eroberer spielt, indem man im inneren Bereich dieser Gruppe von Ländern ein paar Vereinigungen und neue Kombinationen durchführt, hat man schließlich eine Landkarte mit weniger als 1000 Ländern, bei der man wieder weiß, wie man sie