Vom Computer gelöst: berühmte Matheprobleme, bei denen Maschinen geholfen haben (1976–2026)

1976 verkündeten zwei Mathematiker in Illinois, sie hätten bewiesen, dass vier Farben genügen, um jede Landkarte einzufärben, und dass ein Teil ihres Beweises nur von einem Computer überprüft werden konnte. Viele Mathematiker waren zutiefst beunruhigt: Ist es wirklich ein Beweis, wenn kein Mensch ihn vollständig lesen kann? Fünfzig Jahre später hat sich die Frage umgekehrt. 2026 fanden KI-Systeme die Schlüsselideen hinter Ergebnissen, die Fachleute jahrzehntelang nicht gefunden hatten. Dieser Artikel erzählt die Geschichte der Reihe nach und sagt für jedes berühmte Problem genau, was die Maschine getan hat, denn „vom Computer gelöst“ kann sehr Verschiedenes bedeuten.

1976: vier Farben und ein Beweis, den niemand lesen konnte

GCSE-Kernstoff

Die Frage ist einfach genug für die Grundschule: Färbe eine Karte so, dass benachbarte Länder nie dieselbe Farbe haben. Wie viele Farben könnte man brauchen? Francis Guthrie vermutete 1852: vier. Dass man vier brauchen kann, sieht man leicht (siehe Bild unten), aber zu beweisen, dass vier immer reichen, für jede mögliche Karte, widerstand den Mathematikern 124 Jahre lang.

Kenneth Appel und Wolfgang Haken fanden einen Weg zu zeigen, dass jede Karte, die fünf Farben bräuchte, eines von fast zweitausend besonderen Mustern enthalten müsste, und dass sich jedes dieser Muster „wegreduzieren“ lässt. Alle von Hand zu prüfen war unmöglich, also tat es ein Computer, mit über tausend Stunden Rechenzeit. Der Satz war bewiesen, aber auf eine Weise, die veränderte, was „Beweis“ in der Praxis bedeutet.

Wie der Zweifel ausgeräumt wurde: 1996 folgte ein kürzerer Computerbeweis, und 2005 überprüften Georges Gonthier und Benjamin Werner das gesamte Argument im Beweisassistenten Coq. Heute ist er einer der am gründlichsten überprüften Sätze der Mathematik.

1996: der erste Beweis, den ein Computer selbst fand

Bachelor-Vertiefung

Die Robbins-Vermutung fragte, ob drei kurze Regeln genau dieselbe Algebra beschreiben wie die Boolesche Algebra, die Wahr-falsch-Logik in jedem Computerchip. Spitzenlogiker, darunter Alfred Tarski, hatten sie sechzig Jahre lang nicht klären können. 1996 durchsuchte William McCunes automatischer Beweiser EQP etwa acht Tage lang mögliche Schlussketten und fand einen Beweis. Das war etwas grundsätzlich anderes als 1976: Niemand hatte dem Computer gesagt, wie das Argument aussehen sollte.

1998–2014: Keplers Orangen

1611 behauptete Johannes Kepler, dass die Art, wie Obsthändler Orangen stapeln (jede Lage in den Mulden der darunter), die dichteste mögliche Packung gleich großer Kugeln ist. Sie füllt etwa 74 % des Raums (genau π/√18).

Thomas Hales verwandelte die Frage zusammen mit Samuel Ferguson in Tausende von Optimierungsproblemen, löste sie per Computer und verkündete 1998 einen Beweis. Die Gutachter der Zeitschrift erklärten, sie seien sich „zu 99 % sicher“, dass er stimme, könnten aber nicht jede Rechnung prüfen. Hales antwortete mit dem Projekt Flyspeck, das alles in Beweisassistenten-Software erneut überprüfte; es wurde 2014 abgeschlossen.

2016: der 200-Terabyte-Beweis

GCSE-Kernstoff

Hier ist ein Rätsel zum Selbstausprobieren. Färbe jede ganze Zahl rot oder blau. Schaffst du es so, dass kein pythagoreisches Tripel (drei Zahlen mit a² + b² = c², etwa 3, 4, 5) einfarbig ist?

Ronald Graham setzte 100 Dollar für die Antwort aus. 2016 nutzten Marijn Heule, Oliver Kullmann und Victor Marek einen SAT-Solver (Software, die riesige Wahr-falsch-Logikrätsel löst) etwa zwei Tage lang auf dem Supercomputer Stampede. Die Antwort: Jede Zahl von 1 bis 7.824 lässt sich sicher färben, aber 1 bis 7.825 nicht. Der Beweis, dass keine Färbung von 7.825 Zahlen funktioniert, war 200 Terabyte groß, laut Nature damals der größte Mathebeweis aller Zeiten. Dieselbe Technik klärte 2019 Kellers Vermutung über das Pflastern des Raums mit Würfeln in sieben Dimensionen.

2025–2026: KI beginnt, die Ideen zu finden

Master-Vertiefung

Bei allem Bisherigen dienten Computer zum Prüfen oder zum Suchen in einem von Menschen entworfenen Rahmen. Ab 2025 begannen Systeme auf Basis großer Sprachmodelle, die mathematischen Ideen selbst vorzuschlagen, und koppelten sie an den Beweisassistenten Lean, damit das Ergebnis maschinell geprüft und nicht einfach geglaubt werden kann.

Die Einheitsabstands-Vermutung (Mai 2026). 1946 fragte Paul Erdős: Wenn man n Punkte auf eine ebene Fläche setzt, wie viele Paare können genau 1 Einheit voneinander entfernt sein? Er glaubte, die Antwort wachse nur minimal schneller als n. Ein internes Modell von OpenAI fand eine unendliche Familie von Punktmengen, die das um eine echte Potenz von n übertrifft, mit tiefen Werkzeugen der algebraischen Zahlentheorie. Neun führende Mathematiker, darunter die Fields-Medaillenträger Tim Gowers und Jacob Tsimerman, prüften das Ergebnis und schrieben einen Begleitartikel, und Will Sawin machte den Gewinn explizit. Gil Kalai verglich seine Bedeutung mit dem Vierfarbenbeweis von 1976.

AlphaProof Nexus (Mai 2026). Google DeepMind ließ seinen Agenten, der das Modell Gemini mit Lean verbindet, auf 353 offene Probleme aus der Erdős-Problemdatenbank los. Er löste 9, darunter zwei, die 56 Jahre offen waren, und bewies 44 Vermutungen aus der Online-Enzyklopädie der Zahlenfolgen (OEIS). Jeder Beweis kompiliert in Lean. Beachte aber die Erfolgsquote: etwa 2,5 %.

Astra (August 2026). OpenAI verkündete zehn Ergebnisse seines unveröffentlichten nächsten Modells, darunter die erste Konstruktion einer nicht-sofischen Gruppe (eine Antwort auf eine Frage, die Mikhail Gromov 1999 gestellt hatte), drei Erdős-Probleme und die erste Verbesserung seit 1978 einer allgemeinen Schranke für Kugelpackungen. Zu jedem gab es ein Lean-Zertifikat. Eine unabhängige menschliche Prüfung fand keine bestätigten wesentlichen Fehler in den Hauptergebnissen, auch wenn ein Ergebnis eine Fachanfrage nach grundlegender Überarbeitung auslöste; die Begutachtung durch Fachzeitschriften war zum Zeitpunkt des Schreibens nicht abgeschlossen.

Fünfzig Jahre in einer Zeitleiste

Was das bedeutet, wenn du Mathe lernst

Jedes Ergebnis in diesem Artikel hing weiterhin von Menschen ab: Jemand musste das Problem präzise formulieren, entscheiden, welcher Ansatz den Versuch wert war, prüfen, ob der vom Computer bewiesene Satz der war, auf den es ankam, und erklären, warum er wahr ist. Genau diese Fähigkeit baut Schulmathematik auf, wenn sie verlangt, deinen Rechenweg zu zeigen, und das ist auch das Thema unseres Artikels Kann KI wirklich Mathe?. Für die noch offenen Probleme und eine Karte für Karte geordnete Liste dieser gelösten Probleme siehe unsere Übersicht über ungelöste mathematische Rätsel.