Ein Beweis, den keiner allein überblickt

1 Höflicher Beifall

Am 22. Juli 1976 verkündeten zwei Mathematiker der University of Illinois, Kenneth Appel und Wolfgang Haken: Vier Farben genügen. Jede Landkarte in der Ebene lässt sich unter den üblichen Voraussetzungen so färben, dass Gebiete mit einer gemeinsamen Grenzlinie verschiedene Farben haben; eine bloße Berührung in einem Punkt zählt nicht als Nachbarschaft. Im August stellte Haken den Beweis an der University of Toronto auf der gemeinsamen Sommertagung der American Mathematical Society und der Mathematical Association of America vor. Er war achtundvierzig, in Berlin geboren und von Haus aus Topologe, in der Erforschung dreidimensionaler Formen längst ein bekannter Name. Der Saal war voll. Eine Frage, die seit hundertvierundzwanzig Jahren offen gewesen war, hatte ihre Antwort.

Donald Albers saß an diesem Tag im Publikum. Seinem Bericht zufolge hatte er am Ende von Hakens Vortrag mit stürmischem Jubel gerechnet. Stattdessen hörte er höflichen Beifall. Hinterher äußerte ein Mathematiker nach dem anderen sein Unbehagen. Es lag an der Gestalt dieses Beweises: Einen beträchtlichen Teil hatte eine Maschine erledigt, in zwölfhundert Rechenstunden. Kein Mensch konnte das alles von Anfang bis Ende von Hand nachprüfen. In den Hunderten Seiten Computerausdruck, hieß es immer wieder, könnte sich doch irgendwo ein Fehler verbergen. Albers schob an dieser Stelle selbst eine Frage ein: Ob sie womöglich hofften, es möge einer darin sein? Sein Bericht erschien im Frühjahr 1981 in einer mathematischen Zeitschrift. Die erste Hälfte des Titels lautete sinngemäß „Höflicher Beifall“, die zweite fragte: „Was ist heute ein Beweis?“

Die Frage lässt sich so einfach stellen, dass ein Kind sie versteht. Auch ihr Anfang war unspektakulär. 1852 färbte ein junger Mann namens Francis Guthrie eine Karte der englischen Grafschaften und bemerkte, dass vier Farben offenbar immer ausreichten. Er erzählte es seinem Bruder Frederick, der damit zu seinem Lehrer De Morgan ging. Am 23. Oktober schrieb De Morgan an Hamilton in Dublin und reichte die Frage weiter. Ein Student habe ihn heute, so begann der Brief sinngemäß, um eine Begründung für eine Tatsache gebeten, von der er bislang nicht gewusst habe, dass sie eine Tatsache sei, und von der er es noch immer nicht wisse. Drei Tage später antwortete Hamilton, er werde sich wohl nicht so bald mit diesem Quaternion der Farben beschäftigen. Die Quaternionen hatte er neun Jahre zuvor entdeckt. Noch am selben Tag hatte er die Formel in einen Stein einer Brücke geritzt, an der er vorbeikam. In jenen Jahren lebte er ganz in dieser Sache.

Der junge Mann, der die Frage gestellt hatte, war damals einundzwanzig und hatte gerade seinen Abschluss in Rechtswissenschaften gemacht. Später beschäftigte er sich nicht mehr mit dem Problem und schrieb nie auch nur eine Zeile darüber. Er ging nach Südafrika und lehrte mehr als zwanzig Jahre als Professor für Mathematik am South African College in Kapstadt. Was ihm an Zeit und Aufmerksamkeit blieb, galt den Heidekrautgewächsen des Kaps. Gemeinsam mit einem Botaniker arbeitete er daran bis zu seinem Tod. Eine Pflanzengattung trägt seinen Nachnamen.

Weniger als eine Minute braucht man, um die Frage zu stellen. Hundertvierundzwanzig Jahre brauchte es für den Beweis. Doch um das Unbehagen an jenem Tag in Toronto zu verstehen, muss man noch einmal zurück. Denn bewiesen worden war das Ganze schon einmal.

2 Ein Beweis lebt elf Jahre

Über zwanzig Jahre hatte das Problem in der Schublade gelegen. Am 13. Juni 1878 fragte Cayley bei einer Sitzung der London Mathematical Society, ob es inzwischen jemand gelöst habe. Im folgenden Jahr meldete sich ein ehemaliger Schüler. Alfred Kempe, ein Londoner Prozessanwalt, kündigte im Juli 1879 in Nature einen Beweis an; der vollständige Text erschien anschließend in einer amerikanischen Mathematikzeitschrift. Seinen Lebensunterhalt verdiente er vor Gericht, Mathematik hatte er in Cambridge bei Cayley gelernt. Sein Beweis war klar geschrieben und die Idee geschickt: Bilden Gebiete auf einer Karte eine zusammenhängende Kette aus zwei abwechselnden Farben, kann man die Farben in der ganzen Kette vertauschen, ohne die übrige Karte anzutasten. Später nannte man solche Gebilde Kempe-Ketten. Der Beweis wurde anerkannt. Und blieb es elf Jahre lang. Im Jahr darauf legte der schottische Physiker Tait noch zwei Beweise vor, in denen kluge Ideen und grundlegende Fehler nebeneinanderstanden. Vielen galt die Frage in diesen Jahren als erledigt.

1890 zeigte Heawood, damals Mathematikdozent in Durham, wo Kempes Beweis eine Lücke hatte. Für ein Gebiet mit fünf Nachbarn waren zwei aufeinanderfolgende Farbvertauschungen nötig. Kempe hatte angenommen, sie kämen einander nicht in die Quere. Die beiden Ketten können sich auf der Karte aber ineinander verschlingen: Die erste Vertauschung zerstört dann womöglich die Voraussetzung für die zweite. Der Beweis fiel in sich zusammen.

Heawood beließ es nicht beim Einreißen. Mit den brauchbaren Teilen des gescheiterten Beweises bewies er eine schwächere Aussage: Fünf Farben reichen auf jeden Fall. Auch die Technik, die Farben einer ganzen Kette zu vertauschen, blieb erhalten und wurde zu einem gängigen Werkzeug der Graphentheorie. Dass ein gescheiterter Beweis etwas Brauchbares hinterlässt, ist in der Geschichte der Mathematik nichts Ungewöhnliches. Heawood wurde in Durham vom Dozenten zum Professor und war von 1926 bis 1928 Vizekanzler der Universität. Fast sechzig weitere Jahre beschäftigte er sich mit Kartenfärbungen. Seine letzte Arbeit darüber erschien 1949, als er siebenundachtzig oder achtundachtzig war. Seine Kollegen erinnerten sich an einen kleinen, schmächtigen, leicht gebeugten Mann mit gewaltigem Bart, meist in einem seltsam geschnittenen, sichtlich alten Umhang. Bei seinen Vorlesungen durfte ein Hund im Hörsaal bleiben.

Ungewöhnlich ist die Zeitspanne. Elf Jahre lang lag ein klar ausformulierter Beweis vor den Augen erstklassiger Mathematiker, ohne dass jemand seinen Fehler fand. Dass Menschen einen Beweis lesen können, hat noch nie bedeutet, dass ihn tatsächlich jemand geprüft hat. Hier lag die eine Hälfte des Unbehagens von Toronto: Wenn es schon mit einem menschenlesbaren Beweis so stand, worauf sollte das Vertrauen in einen beruhen, den niemand mehr durchlesen konnte?

3 Im Rechenzentrum von Illinois

Schon vor Appel und Haken hatte der Deutsche Heinrich Heesch auf diesem Weg Computer eingesetzt. In den sechziger Jahren hatte er eine entscheidende Methode ausgearbeitet. 1967 suchte Haken ihn wegen des Problems auf. In den folgenden vier Jahren reiste Heesch mehrmals in die USA, wo die Rechner größer und schneller waren; zu denen, mit denen er dort zusammenarbeitete, gehörte Haken. Ausgerechnet in der entscheidenden Phase stellte die Deutsche Forschungsgemeinschaft seine Förderung ein.

Anfang der siebziger Jahre berichtete Haken in einem Vortrag von ihren Versuchen am Computer des Brookhaven-Laboratoriums. Computerfachleute hätten ihm erklärt, auf diesem Weg sei nichts zu machen. Nach dem Vortrag sprach ihn Appel an, ein Kollege aus demselben Fachbereich. Die Experten irrten sich, sagte er. Es werde dauern, aber es sei machbar. 1972 begannen die beiden zusammenzuarbeiten. Appel kümmerte sich vor allem um die Berechnungen, Haken um die theoretische Seite.

Sie schrieben nicht erst einen herkömmlichen Beweis und ließen zum Schluss ein paar Zahlen ausrechnen. Die Maschine war von Anfang an Teil einer Rückkopplung: Die Menschen legten Regeln fest, der Rechner probierte sie aus; was dabei schiefging, kam zu den Menschen zurück, die ihre Regeln änderten und sie wieder in den Rechner schickten. So ging es mehrere Jahre. Am Ende standen 487 Regeln, rund zehntausend von Hand betrachtete lokale Fälle und ungefähr zweitausend Muster, die die Maschine einzeln überprüfte. Manche dieser Muster beanspruchten auf dem langsameren Rechner neunzig Minuten, auf dem schnelleren immer noch dreißig. Insgesamt kamen etwa zwölfhundert Stunden Maschinenzeit zusammen. Nach ihrer eigenen Angabe trafen die Computer dabei rund zehn Milliarden logische Entscheidungen. Für die letzte Etappe bekamen die beiden Rechenzeit auf einer Großanlage, die die University of Illinois im März 1976 eigentlich für ihre Verwaltung angeschafft hatte.

Und auch die Handarbeit erledigten nicht allein die beiden Autoren. Die letzte Fassung der Regeln wurde von Hand hergeleitet. In der ersten Hälfte des Jahres 1976 arbeiteten sich Appel, Haken und Hakens Tochter Dorothea monatelang durch jedes der 1.936 Muster, aus denen später die Liste bestand. Dorothea ging in diesen Jahren erst noch zur Schule und dann an die Universität; später wurde sie selbst Informatikerin. Vor der Bekanntgabe des Beweises holten die beiden Familien fünf ihrer Kinder dazu: Dorothea und Armin Haken sowie Laurel, Peter und Andrew Appel. Seite für Seite verglichen sie die in der Arbeit gezeichneten Muster mit den Computerausdrucken und suchten nach Übertragungsfehlern. Appels Tochter Laurel war dreizehn und prüfte gut siebenhundert Seiten. Haken erinnerte sich später sinngemäß: Einen ganzen Monat habe sie daran gearbeitet und etwa achthundert Fehler gefunden. Achthundert auf siebenhundert Seiten, das sei nicht viel. Sechshundertfünfzig habe sie selbst korrigiert; für den Rest hätten Appel und er nur fünf Tage gebraucht.

Die Liste änderte sich fortwährend. Im Vorabdruck umfasste sie 1.936 Muster, in der veröffentlichten Fassung noch 1.482; später wurde sie weiter auf etwa 1.405 gestrafft. Die eigentliche Arbeit erschien 1977 in zwei Teilen. Am Teil über die Überprüfung war auch John Koch beteiligt. Hinzu kamen rund 450 Seiten auf Mikrofiche mit zahlreichen Zeichnungen und Prüfprotokollen. Appel und Haken hatten selbst abgeschätzt, wie lange ein Mensch allein für die vollständige Rechnerausgabe zu einem schwierigen Muster brauchen würde: mehrere Jahre, bei vierzig Stunden Prüfarbeit pro Woche. Mehr als ein Jahrzehnt später, 1989, veröffentlichten die beiden den gesamten Beweis noch einmal als Buch.

Im Herbst 1976 ließ der Fachbereich Mathematik der University of Illinois seine Frankiermaschine ändern. Auf jedem Brief, der ihn verließ, stand nun ein Satz: Vier Farben genügen.

4 Eine Liste

Die Maschine arbeitete die Einträge einer Liste ab. Was war das für eine Liste, und weshalb ging es nicht ohne sie? Dazu muss man sich die Form von Kempes Beweis ansehen. Der Beweis von 1976 hatte dasselbe Gerüst wie der von 1879. Man nimmt zunächst an, vier Farben reichten nicht. Dann muss es ein kleinstes Gegenbeispiel geben: unter allen Karten, die fünf Farben brauchen, eine mit der geringsten Zahl von Gebieten. Nun benötigt man zweierlei. Erstens eine Liste lokaler Muster und den Nachweis, dass jede Karte mindestens eines davon enthalten muss. Die Liste heißt dann unvermeidbar. Die Methode dafür nennt sich Entladung: Jedes Gebiet erhält zunächst eine Zahl, abhängig davon, wie viele Nachbarn es hat. Anschließend werden diese Zahlen nach festen Regeln zwischen benachbarten Gebieten verschoben. Irgendwo muss am Ende eine positive Zahl übrig bleiben, und dort findet sich zwangsläufig eines der Muster aus der Liste. Zweitens muss man für jedes einzelne Muster nachweisen, dass es in einem kleinsten Gegenbeispiel unmöglich vorkommen kann. Taucht es auf, lässt es sich zusammenziehen; es entsteht eine kleinere Karte, die sich nach Voraussetzung mit vier Farben färben lässt. Fügt man das entfernte Stück wieder ein, lassen sich die Farben immer noch passend verteilen. Das nennt man reduzierbar. Zusammen ergibt beides einen Widerspruch: Das kleinste Gegenbeispiel müsste etwas aus der Liste enthalten und dürfte nichts aus ihr enthalten. Also gibt es keines. Die Entladungsmethode hatten Appel und Haken von Heesch übernommen.

Kempes Liste war kurz. Er zeigte zunächst, dass auf jeder Karte ein Gebiet mit höchstens fünf Nachbarn vorkommt. Mit bis zu vier Nachbarn kam sein Verfahren der Farbvertauschung zurecht. Im Fall der fünf Nachbarn fand Heawood die Lücke.

Der weitere Weg bestand darin, diesen einen Fall mit fünf Nachbarn aufzuteilen und durch größere, genauer unterschiedene Muster zu ersetzen, deren Reduzierbarkeit sich jeweils einzeln beweisen ließ. Doch je feiner man aufteilte, desto länger wurde die Liste und desto aufwendiger die Prüfung jedes Eintrags. Um ein Muster liegt ein Ring von Gebieten. Man muss jede mögliche Anordnung der vier Farben auf diesem Ring durchgehen und prüfen, ob sich die Färbung passend ändern lässt. Bei vierzehn Gebieten im Ring sind das annähernd zweihunderttausend Anordnungen, bei achtzehn mehr als sechzehn Millionen.

Darum kamen Appel und Haken um die Maschine nicht herum. Es ging nicht um eine Vorliebe für Computer. Das Gerüst lag seit Kempe fest: Entweder fand man eine kurze Liste, oder man prüfte eine lange Liste Eintrag für Eintrag. Eine kurze hatte in hundert Jahren niemand gefunden.

5 Dreierlei Unbehagen

Hinter dem Unbehagen jenes Tages in Toronto ließen sich später drei verschiedene Einwände erkennen. Sie meinten nicht dasselbe.

Der erste Einwand lautete: Das ist kein Beweis. Am bekanntesten formulierte ihn 1979 der Philosoph Thomas Tymoczko. Er behauptete nicht, der Vierfarbensatz sei wahrscheinlich falsch. Sein Punkt war ein anderer. Ein Beweis habe zwei Aufgaben: Er soll von der Wahrheit des Ergebnisses überzeugen, und er soll ermöglichen, den ganzen Gedankengang von Anfang bis Ende zu verfolgen und sein Warum zu erkennen. Die zweite Eigenschaft nannte er sinngemäß Überschaubarkeit: Ein Einzelner kann das Ganze von einem Standpunkt aus überblicken. Der Beweis von 1976 erfüllte die erste Aufgabe, hatte aber die zweite aufgegeben. Wenn man auch eine solche unüberschaubare Berechnung als Beweis anerkenne, habe man die Bedeutung des Wortes bereits erweitert.

Der zweite Einwand lautete: Es ist ein Beweis, aber kein schöner. Er erklärt nicht, warum ausgerechnet vier Farben genügen. Viele im Saal von Toronto hofften, irgendwann werde ein kurzer Beweis auftauchen, der einem den Grund verständlich macht.

Der dritte Einwand war der praktischste: Vielleicht ist es ein Beweis, aber wie prüft man, ob er wirklich fehlerfrei ist? Ist das Programm korrekt? Fehlt etwas auf der Liste? Wurde eine der Tausenden Ausgaben falsch behandelt? Sind gedruckte Daten bei der Weitergabe durcheinandergeraten? Im selben Jahr schrieben DeMillo, Lipton und Perlis in einem Aufsatz, die Verlässlichkeit eines Beweises komme nie allein aus seinen formalen Ableitungen. Sie entstehe auch dadurch, dass er nach seinem Eintritt in die mathematische Gemeinschaft kritisiert, vereinfacht, weiterverwendet und gelehrt werde. Wo sollte dieser Prozess bei einem Beweis beginnen, den niemand vollständig nachprüfen konnte?

Was später geschah, beantwortete eigentlich nur den dritten Einwand. In den neunziger Jahren wollten Robertson, Sanders, Seymour und Thomas zunächst den Beweis von Appel und Haken überprüfen. Sie gaben diesen Versuch bald auf. Später schrieben sie sinngemäß: Ein Teil des Beweises sei computergestützt und lasse sich deshalb nicht von Hand kontrollieren; der Teil, der angeblich von Hand überprüfbar sei, erweise sich hingegen als außerordentlich verwickelt und kleinteilig. Schon die Beschreibungen von mehr als tausend Mustern einzeln einzugeben, wäre ein gewaltiges Unternehmen gewesen. Also machten sie es selbst noch einmal. 1996 waren sie fertig. Ihre Liste hatte nur noch 633 Einträge, die Zahl der Entladungsregeln sank von mehreren Hundert auf zweiunddreißig. Programme und Daten wurden veröffentlicht, sodass andere die Rechnung selbst wiederholen konnten. Für die Überprüfung des Unvermeidbarkeitsbeweises, schrieben sie, brauche man von Hand mehrere Monate, am Computer ungefähr zwanzig Minuten. Die Maschine war nicht verschwunden. Aber ihr Anteil war nun erstmals etwas, das andere unabhängig überprüfen konnten. 2005 übertrug Gonthier diesen modernen Beweis vollständig in ein formales System innerhalb eines sogenannten Beweisassistenten. Ein sehr kleines Kernprogramm prüfte dort Schritt für Schritt nach. Geprüft wurde der Weg von 1996, nicht der Programmcode, den Appel und Haken 1976 hatten laufen lassen. Dass jene damaligen Programme fehlerfrei waren, hat bis heute niemand auf diese Weise bewiesen. Vertrauen musste man nun nicht mehr Tausenden von Fällen und einem umfangreichen Spezialprogramm, sondern diesem kleinen Kern, den formalen Definitionen und dem Schritt, der die ursprüngliche Behauptung in die formale Sprache übersetzte. Das Vertrauen verschwand nicht. Es wurde auf weniger Stellen konzentriert, und andere konnten die Prüfung an diesen Stellen übernehmen.

Der zweite Einwand blieb unbeantwortet. Im März 2026 schlugen sechs Autoren in einem Vorabdruck einen neuen Beweis und ein wesentlich schnelleres Färbeverfahren vor. Sie verwendeten 8.202 reduzierbare Konfigurationen, darunter zwei einfache Fälle. Mit Stand vom 1. Oktober 2026 ist dies als neuer Beweisvorschlag der Autoren zu bezeichnen, nicht als ein Ergebnis, über das nach langjähriger unabhängiger Überprüfung bereits Einigkeit besteht. Diese Vorsicht ist ebenso wenig ein Urteil, der Beweis sei falsch. Thomassen, einer der Beteiligten, sagte, er wünsche sich einen Beweis ohne Computer. Er habe nie aufgehört, darüber nachzudenken.

6 Ein Satz, der in kein Buch passt

Das zweite Beispiel ist größer. So groß, dass kein einzelnes Buch es aufnehmen kann.

In der vorigen Folge war von einem Gerüst die Rede: Je zwei Elemente lassen sich verknüpfen, eines tut dabei gar nichts, und zu jedem gibt es ein Element, das seine Wirkung aufhebt. Mathematiker nennen das eine Gruppe. Zerlegt man sie mithilfe von Normalteilern und den zugehörigen Quotientengruppen, gelangt man zu einfachen Gruppen: solchen ohne nichttrivialen echten Normalteiler. Das bedeutet keineswegs, dass sie keine nichttrivialen Untergruppen haben. Sie spielen eine ähnliche Rolle wie die Primzahlen. Jede ganze Zahl lässt sich aus Primzahlen zusammensetzen, jede endliche Gruppe besitzt eine Kompositionsreihe mit einfachen Gruppen als Faktoren. Diese Faktoren legen aber nicht eindeutig fest, wie die ursprüngliche Gruppe zusammengesetzt ist. Welche endlichen einfachen Gruppen gibt es also überhaupt?

Die kleinsten sind schlicht: zyklische Gruppen mit einer Primzahl von Elementen. Dreht man ein regelmäßiges Fünfeck jeweils um ein Fünftel einer vollen Umdrehung, ist man nach fünf Schritten wieder am Anfang. Die fünf möglichen Drehungen bilden eine einfache Gruppe. Die kleinste einfache Gruppe, bei der es auf die Reihenfolge der Verknüpfung ankommt, hat sechzig Elemente: die sämtlichen Drehungen eines regelmäßigen Ikosaeders. Dass es für Gleichungen fünften Grades keine allgemeine Lösungsformel durch Wurzeln gibt, war Thema der zehnten Folge. Geht man der Sache auf den Grund, steht einem genau diese einfache Gruppe mit sechzig Elementen im Weg.

Die Antwort ist eine Liste. Einige unendliche Familien, deren Mitglieder nach festen Regeln aufeinanderfolgen, und dazu sechsundzwanzig verstreute Ausnahmen, die zu keiner dieser Familien gehören. Die größte Ausnahme erhielt später den Namen Monster. Die Anzahl ihrer Elemente ist eine vierundfünfzigstellige Zahl. Um 1973 sagten Fischer und Griess ihre Existenz voraus. Am 14. Januar 1980 verkündete Griess in Ann Arbor, er habe sie konstruiert: als die Gesamtheit der Symmetrien eines 196.883-dimensionalen Objekts. Als er die Arbeit 1982 veröffentlichte, nannte er das Monster den freundlichen Riesen.

Zuerst waren einzelne Aufsätze immer länger geworden. 1963 bewiesen Feit und Thompson, dass jede endliche Gruppe ungerader Ordnung auflösbar ist. Jede nichtkommutative endliche einfache Gruppe muss folglich eine gerade Ordnung haben. Ihre Arbeit war 255 Seiten lang und füllte eine ganze Zeitschriftenausgabe. Später überführte Gonthier mit einem Team den gesamten Beweis in einen Beweisassistenten. Die Arbeit dazu erschien 2013.

Der Nachweis, dass diese Liste vollständig ist, heißt Klassifikationssatz für endliche einfache Gruppen. Er ist weder ein Aufsatz noch ein Buch. Er besteht aus Hunderten von Aufsätzen von etwa hundert maßgeblich beteiligten Autoren, mit rund zehntausend Seiten eigentlichem Beweistext. Zählt man die nötigen Hintergrundresultate hinzu, kommt eine häufig genannte Schätzung auf fünfzehntausend Seiten. Eine einheitliche Zählweise gibt es nicht. Denn wo dieser eine Beweis eigentlich endet, lässt sich gar nicht sauber angeben.

Anfang der achtziger Jahre veröffentlichte Daniel Gorenstein ein Buch, dessen Titel übersetzt etwa „Endliche einfache Gruppen: Einführung in die Klassifikation“ lautet. Darin fasste er mehr als zwanzig Jahre Arbeit als ein abgeschlossenes Ganzes zusammen. Über zwei Jahrzehnte hatte er den Überblick über das Unternehmen behalten und seine Richtung mitbestimmt. Aschbacher, einer der am tiefsten Beteiligten, schrieb später im Rückblick, in der mathematischen Gemeinschaft habe allgemein die Auffassung geherrscht, die Klassifikation sei um 1980 abgeschlossen gewesen.

Abgeschlossen: Das war kein einzelner Satz, den an einem bestimmten Tag jemand auf einer Bühne aussprach. Ein Forschungsprogramm wurde nach und nach zu einem anerkannten Ergebnis. Als Grundlage diente die Überzeugung, alle großen Zweige seien abgedeckt und für das, was noch fehlte, wüssten die zuständigen Fachleute bereits, wie es zu behandeln sei.

Dass Fachleute wissen, wie sie etwas zu Ende bringen können, ist etwas anderes als ein vollständig veröffentlichter Beweis, auf dessen einzelne Schritte man verweisen kann. Genau zwischen diesen beiden Aussagen lag das Problem.

7 Das fehlende Stück

Ein ganzer Zweig des Klassifikationsbaums betraf die sogenannten quasidünnen Gruppen. Im Plan der ersten Generation war Geoff Mason dafür zuständig. 1980 gab er die Klassifikation dieses Bereichs bekannt, 1981 lag ein etwa achthundertseitiges Manuskript vor. Es wurde nicht veröffentlicht. Erst später zeigte sich, dass es unvollständig war und schwerwiegende Lücken enthielt.

Diese Lücke hat keinen Tag ihrer Entdeckung. Es war nicht wie 1890, als Heawood auf einen bestimmten Schritt bei Kempe zeigen konnte: Hier stimmt es nicht. Die Einsicht setzte sich allmählich durch. Als man den Klassifikationsbeweis von den späten achtziger bis in die neunziger Jahre neu ordnete, ließ sich dieser Teil immer weniger als abgeschlossen behandeln. Was längst fertig zu sein schien, war tatsächlich noch nicht fertig.

Geschlossen haben die Lücke Aschbacher und Stephen Smith. 2004 veröffentlichten sie „The Classification of Quasithin Groups“ in zwei Bänden, zusammen etwa 1.220 Seiten. Keine einzelne Seite mit Berichtigungen: ein neues Buch. Danach kamen noch einige kleinere Auslassungen zum Vorschein, die ebenfalls nach und nach behoben wurden.

Drei Aussagen lassen sich also festhalten. Die mathematische Gemeinschaft hatte die Liste Anfang der achtziger Jahre bereits als richtig anerkannt. In der öffentlich zugänglichen Beweisliteratur der ersten Generation war tatsächlich ein großer Teil unvollendet geblieben. Die beiden Bände von 2004 lieferten für diesen Teil eine vollständige, publikationsreife Behandlung.

Gorenstein hatte früh begriffen, dass selbst ein richtiger Beweis in der Gestalt der ersten Generation keinen vernünftigen Endzustand darstellte. Mit Richard Lyons und Ronald Solomon begann er ein Projekt der zweiten Generation: Den über Hunderte von Aufsätzen verstreuten Beweis wollten sie als systematische, möglichst in sich geschlossene Folge von Monographien neu schreiben, mit klar erkennbaren Abhängigkeiten zwischen den Ergebnissen. Im August 1992 starb Gorenstein. Der erste Band dieser zweiten Generation erschien erst 1994. Der Verlag beschrieb das Ziel der Reihe als einen sorgfältigen, weitgehend in sich geschlossenen Beweis. Band zehn erschien 2023; seither wird weiter an der Neufassung gearbeitet. Angaben zur Zahl der Bände und zum Gesamtumfang müssen deshalb mit den Veröffentlichungen fortgeschrieben werden. Lyons und Solomon schreiben an den letzten Teilen des Hauptstrangs. In Deutschland hat Stroth außerdem ein umfangreiches Manuskript für den abschließenden Abschnitt in Arbeit. Die ursprünglich veranschlagten zwölf Bände und fünftausend Seiten wirken inzwischen knapp bemessen.

Hat ein einziger Mensch den Beweis der ersten Generation samt sämtlichen Ergebnissen, auf die er sich stützt, von Anfang bis Ende Zeile für Zeile gelesen? Es lässt sich niemand finden, der das von sich behauptet. Aschbacher, Lyons und Solomon haben einen außergewöhnlichen Überblick über das gesamte Bauwerk; daneben hat jeder Bereich seine eigenen Fachleute. Aber die Struktur zu beherrschen und Hunderte von Aufsätzen Seite für Seite zu prüfen, sind Arbeiten von ganz unterschiedlicher Größenordnung.

Die Mathematik sucht in der Praxis auch nicht nach einem übermenschlichen Leser. Die Fachleute jedes Gebiets stehen für ihren jeweiligen Teil ein. Ergebnisse aus verschiedenen Aufsätzen werden immer wieder aufgerufen. Das eröffnet Gelegenheiten zur erneuten Prüfung, garantiert aber nicht, dass bei jedem Verweis jemand alles noch einmal Zeile für Zeile kontrolliert. Wird eine große Lücke entdeckt, schreibt man neu. Übersichtsarbeiten und die Monographien der zweiten Generation sollen schließlich aus der Frage, wer wem vertraut, möglichst genau die Frage machen, welches Ergebnis von welchem anderen abhängt. Dass ein Satz bekannt ist, heißt nicht, dass ein einzelner Mensch alle seine Einzelheiten kennt.

8 Dreimal fertig

Es gibt noch ein drittes Beispiel. 1611 schrieb Kepler ein kleines Buch über sechseckige Schneeflocken, als Neujahrsgeschenk für seinen Förderer. Beiläufig stellte er darin eine Vermutung auf: So, wie man auf dem Obstmarkt Orangen Schicht für Schicht zu einer Pyramide stapelt, liegen sie bereits so dicht wie nur möglich im Raum. Angefangen hatte die Frage bei Kanonenkugeln. Walter Raleigh hatte seinen Gehilfen Harriot nach einer Methode suchen lassen, die Zahl der Kugeln in einem Stapel zu bestimmen. Seit 1606 stand Harriot mit Kepler im Briefwechsel. 1900 nahm Hilbert das Problem in seine Liste auf, als Teil der achtzehnten Aufgabe. 1998 kündigte Thomas Hales einen Beweis an. Die eine Hälfte bestand aus herkömmlichen mathematischen Argumenten, die andere aus der Überprüfung zahlreicher Ungleichungen, linearer Optimierung und endlichem Durchzählen. Sein Doktorand Samuel Ferguson leistete bei einem entscheidenden Teil einen wesentlichen Beitrag.

Die Annals of Mathematics stellten dafür eine Gutachtergruppe von ungefähr zwölf Personen zusammen, die rund vier Jahre mit der Prüfung verbrachte. 2003 erklärte ihr Leiter Fejes Tóth, man sei zu neunundneunzig Prozent von der Richtigkeit des Beweises überzeugt, könne aber nicht sämtliche Berechnungen zertifizieren. Diese Zahl wurde später unzählige Male zitiert. Sie bezifferte etwas, das beim wissenschaftlichen Begutachten meist unausgesprochen bleibt: Es ist kein Schalter, der nur die Stellungen richtig und falsch kennt. 2005 veröffentlichten die Annals die Hauptargumentation auf den Seiten 1065 bis 1185, insgesamt 121 Seiten. Die Rechenmaterialien und die zugehörigen Arbeiten über die Berechnungen wurden gesondert bereitgestellt oder veröffentlicht.

Hales beließ es nicht dabei. Er rief ein Projekt ins Leben, das den gesamten Beweis in ein formales System übertragen sollte. Ein kleiner maschineller Prüfkern würde ihn kontrollieren; kein Gutachter sollte die Berechnungen einfach glauben müssen. Am 10. August 2014 meldete das Projekt den Abschluss. Zwei Beweisassistenten waren dafür zum Einsatz gekommen. 2017 erschien der formale Beweis als Veröffentlichung, unterzeichnet von zweiundzwanzig Autoren.

Ein und derselbe Satz, drei Daten, drei Bedeutungen von fertig. 1998 hielten die Autoren ihre Arbeit für abgeschlossen. 2005 hielt die Zeitschrift das Ergebnis für verlässlich genug, um es zu veröffentlichen. 2014 hatte ein formaler Prüfkern die Kontrolle beendet.

Zum vierten Mal begegnet uns diese Frage in der Reihe. In der dritten Folge ging es darum, ob jenes Buch als Anfang der Axiomatisierung gelten kann; in der fünften, ob jene Kommentare Beweise sind; in der neunten, ob jene Reihen schon Infinitesimalrechnung sind. Die ersten drei Male wurde gefragt, wie etwas zu nennen sei, und immer stellten Spätere die Frage rückblickend. Diesmal liegt die Sache anders. Der Gegenstand ist da, sein Name ist unstrittig. Gefragt wird, ob er als gewusst gelten kann. Und diesmal fragen die Zeitgenossen selbst. Als sich 1976 der Saal in Toronto leerte, äußerten die Mathematiker bereits ihr Unbehagen. Drei Jahre später machte Tymoczko daraus eine ausdrückliche Frage.

Die Gegenstimmen waren allerdings immer da. 1980 antwortete Krakowski auf Tymoczko, jeder formale Beweis endlicher Länge sei grundsätzlich überschaubar; die Menschen müssten nur lernen, etwas länger zu leben. Der Satz war spöttisch, enthielt aber einen harten Kern: Die Mathematik hat noch nie verlangt, dass das gesamte Hintergrundwissen zu einem Beweis gleichzeitig in einen einzigen Kopf passt. Ein zwanzigseitiger Aufsatz kann Sätze aus mehreren Tausend Buchseiten heranziehen. Niemand würde deshalb sagen, auf diesen zwanzig Seiten stehe kein Beweis. Thurston schrieb 1994, Mathematiker suchten nach Möglichkeiten, Menschen zum Verstehen und Nachdenken über Mathematik zu bringen. So gesehen muss ein Beweis mehr leisten, als die Wahrheit eines Ergebnisses zu sichern: Er muss den Menschen etwas an die Hand geben. Das Problem großer Beweise ist nicht, dass niemand alles besitzt. Auch in der gewöhnlichen Mathematik besitzt niemand alles. Das Problem ist die Länge der Vertrauenskette. Eine gute Antwort darauf ist, ihre einzelnen Glieder möglichst klein zu halten, sodass die Prüfung von anderen übernommen werden kann.

Was sich seit 1976 tatsächlich verändert hat, lässt sich deshalb nicht als Übergabe der Mathematik vom Menschen an die Maschine beschreiben. Drei Aufgaben, die zuvor eng miteinander verbunden waren, haben sich erstmals in großem Maßstab voneinander getrennt: zu entscheiden, ob ein Argument trägt, ob es Verständnis vermittelt und ob es sich tatsächlich überprüfen lässt. Beim Vierfarbensatz gerieten die Berechnungen aus dem Blickfeld eines Einzelnen, bei der Klassifikation die Literatur und das Spezialwissen. Die Formalisierung versucht, all das wieder in einem Gegenstand zusammenzuführen, den eine Maschine Schritt für Schritt kontrollieren kann. Sie beantwortet einen großen Teil der Frage, worauf Menschen ihr Vertrauen gründen dürfen. Ein anderer Teil bleibt: Wenn die mathematische Gemeinschaft verlässlich weiß, dass etwas wahr ist, versteht sie dann auch schon, warum es wahr ist?

Was keiner allein in der Hand halten kann, lässt sich in Stücke zerlegen, für die sich jeweils eine Hand findet.

1977 stellten drei junge Männer am MIT ein Verschlüsselungsverfahren vor. Es beruhte auf einer mathematischen Schwierigkeit: Zwei große Primzahlen zu multiplizieren ist leicht; aus dem Produkt wieder seine Faktoren zu gewinnen ist schwer. Fünf Jahre später bekam das Verfahren eine Firma, im sechsten Jahr ein Patent.

Weitergerechnet wird. Was aber als Mathematik zählt, ist noch nie abschließend ausgerechnet worden.

Quellen und weiterführende Lektüre

Die folgenden Quellen belegen historische Einzelheiten und unterschiedliche Deutungen im Text. Sammlungskataloge, antike Literatur und moderne Rekonstruktionen sind nicht dieselbe Art von Belegen.

• Vorabdruck von 2026 zum Vierfarbensatz und zu einem nahezu linearen Färbeverfahren
• Forschungsankündigung zum neuen Vierfarbenbeweis von 1996
• Gonthiers formaler Beweis des Vierfarbensatzes
• Originalarbeit zum maschinell geprüften Satz über Gruppen ungerader Ordnung
• Die Klassifikation der quasidünnen Gruppen: Originalmonographie
• Hales’ Beweis der Keplerschen Vermutung in den Annals
• Der formale Beweis der Keplerschen Vermutung von 2017