KI löst offene Matheprobleme: Was steckt dahinter?

Kann eine Maschine Mathematik erfinden? Im Herbst 2026 ist diese Frage aus dem Labor in die Schlagzeilen gewandert. Am 8. September 2026 verkündete das KI-Unternehmen OpenAI, ein internes System habe einen Beweis zu den Navier-Stokes-Gleichungen gefunden, einem der sieben Millennium-Probleme, für deren Lösung je eine Million US-Dollar ausgelobt ist. Am 6. Oktober legte das Unternehmen nach und veröffentlichte Hunderte Manuskripte mit weiteren neuen Resultaten.

Die Reaktionen schwanken zwischen Staunen und Ärger. Manche Fachleute sprechen von einer neuen Epoche, andere warnen vor überhasteten Ankündigungen und offenen Fragen der Urheberschaft. Dieser Beitrag fasst zusammen, was bisher bekannt ist (Stand: 9. Oktober 2026), und zeigt, dass die Idee vom maschinellen Beweisen viel älter ist als jedes Sprachmodell.

Worum es beim Navier-Stokes-Problem geht

Die Navier-Stokes-Gleichungen beschreiben, wie sich zähe Flüssigkeiten und Gase bewegen: Wasser im Rohr, Luft am Flugzeugflügel, Wolken in der Atmosphäre. Sie stammen aus dem 19. Jahrhundert, benannt nach dem Franzosen Claude-Louis Navier und dem Iren George Gabriel Stokes. Ingenieurinnen und Wetterdienste rechnen täglich mit ihnen, doch eine Grundfrage war bisher ungeklärt: Bleibt eine anfangs glatte Strömung in drei Dimensionen für alle Zeiten glatt, oder kann sie in endlicher Zeit eine Singularität entwickeln, eine Stelle, an der etwa die Geschwindigkeit unendlich groß wird?

Das Clay Mathematics Institute nahm diese Frage im Jahr 2000 in seine Liste der Millennium-Probleme auf. Die offizielle Aufgabenstellung lässt mehrere Antworten zu: Man kann zeigen, dass Lösungen immer glatt bleiben, oder ein Gegenbeispiel finden, bei dem eine Strömung zusammenbricht. Für das Gegenbeispiel ist auch eine Variante erlaubt, in der eine glatte äußere Kraft auf die Flüssigkeit wirkt.

Was OpenAI behauptet

Nach Angaben von OpenAI arbeitete ein System aus mindestens 10.000 parallel laufenden KI-Agenten 88 Stunden lang an dem Problem. Das Ergebnis sei ein Beweis, dass eine anfangs ruhende, glatte Flüssigkeit unter einer glatten äußeren Kraft in endlicher Zeit eine Singularität entwickeln kann. Dazu veröffentlichte das Unternehmen eine Arbeit von über 160 Seiten und eine Fassung in Lean, einer Programmiersprache, in der ein Computer jeden Beweisschritt nachprüft.

Damit betrifft der Beweis die Variante mit äußerer Kraft, die das Clay-Institut ausdrücklich zulässt. Mehrere Fachleute weisen allerdings darauf hin, dass sie vor allem der Fall ohne äußere Kraft interessiert, und dieser bleibt offen. OpenAI erklärte, das Preisgeld nicht beanspruchen zu wollen.

Am 6. Oktober folgte ein zweiter Schritt. Auf der Plattform GitHub stellte OpenAI Manuskripte mit neuen Ergebnissen aus vielen Gebieten der Mathematik bereit, nach Zählungen von Fachmedien mehr als 700 Arbeiten in rund 370 Themengruppen. Ein Teil davon ist in Lean formalisiert, weitere Formalisierungen sollen folgen. Im Durchschnitt habe ein Ergebnis so viel Rechenleistung gekostet wie etwa drei Stunden Nachdenken des Abo-Modells ChatGPT Pro.

Wie die Fachwelt reagiert

Das Clay Mathematics Institute erklärte am 11. September sinngemäß, das Problem scheine geklärt zu sein, die Prüfung und die Frage der Anerkennung würden aber bewusst ohne Eile behandelt. Ein Preis wird grundsätzlich erst vergeben, wenn eine Lösung in begutachteten Fachzeitschriften erschienen ist und sich in der Fachwelt bewährt hat.

Am selben Tag veröffentlichten Fields-Medaillenträgerinnen und -träger eine Erklärung mit dem Titel A Severe Misalignment of AI in Mathematics, die inzwischen mehr als zwei Dutzend von ihnen unterzeichnet haben. Sie warnen davor, berühmte offene Probleme als Messlatte für KI zu behandeln, wenn dabei das menschliche Verständnis auf der Strecke bleibt.

Hinzu kommt ein Streit um die Urheberschaft. Kurz vor OpenAIs Ankündigung teilten der New Yorker Mathematiker Tristan Buckmaster und Levent Alpöge mit, dass sie mithilfe von KI-Modellen an eng verwandten Ergebnissen gearbeitet hatten. Ob deren Arbeit OpenAIs System beeinflusst haben könnte, ist umstritten. OpenAI weist das zurück.

Auf die Veröffentlichung im Oktober reagierten viele Fachleute beeindruckt. Der Mathematiker Steven Strogatz nannte die Resultate atemberaubend. Andere mahnen zur Vorsicht: Andrew Sutherland vom MIT erwartet, dass die meisten Ergebnisse stimmen oder sich reparieren lassen, einige Beweise aber ernste Fehler enthalten könnten. Er fordert, auch die gescheiterten Versuche offenzulegen. Am Institute for Advanced Study in Princeton hat sich zudem eine Beratungsgruppe gebildet, zu der unter anderem Timothy Gowers und Martin Hairer gehören. Ihre Leitlinien verlangen unter anderem, dass KI-Labore nach älteren Arbeiten suchen und deren Urheber nennen.

Ein alter Traum: Rechnen statt Streiten

Die Vorstellung, dass Maschinen Wahrheiten ausrechnen könnten, ist über 300 Jahre alt. Gottfried Wilhelm Leibniz träumte im 17. Jahrhundert von einer exakten Zeichensprache für alles Denken. Wenn zwei Gelehrte stritten, sollten sie sich nur noch an den Tisch setzen und sagen: Lasst uns rechnen, auf Latein calculemus. Leibniz baute auch eine der ersten Rechenmaschinen, die alle vier Grundrechenarten beherrschte.

Im 20. Jahrhundert wurde aus dem Traum eine präzise Frage. David Hilbert stellte 1928 das Entscheidungsproblem: Gibt es ein Verfahren, das für jede mathematische Aussage mechanisch entscheidet, ob sie beweisbar ist? Kurt Gödel zeigte 1931, dass jedes hinreichend starke formale System wahre Aussagen enthält, die es nicht beweisen kann. 1936 bewies Alan Turing mit seiner gedachten Rechenmaschine, dass es ein solches allgemeines Entscheidungsverfahren nicht gibt. Mehr dazu steht in der Mathematik des 20. Jahrhunderts.

Diese Grenzen gelten auch für heutige KI. Sie verbieten aber nicht, dass Maschinen in einzelnen Fällen Beweise finden. Genau das tun sie seit Jahrzehnten.

Maschinen beweisen schon lange mit

1. 1956 Das Programm Logic Theorist von Allen Newell, Herbert Simon und Cliff Shaw beweist 38 der ersten 52 Sätze aus dem zweiten Kapitel der Principia Mathematica von Russell und Whitehead, einen davon eleganter als das Original.
2. 1976 Kenneth Appel und Wolfgang Haken beweisen den Vierfarbensatz mit über 1.000 Stunden Rechenzeit. Viele Mathematiker zweifeln, weil kein Mensch alle Fälle selbst prüfen kann.
3. 1996 Das automatische Beweisprogramm EQP von William McCune löst die Robbins-Vermutung, eine über 60 Jahre alte Frage der Algebra.
4. 1998 Thomas Hales legt einen computergestützten Beweis der Kepler-Vermutung über die dichteste Kugelpackung vor. Nach jahrelanger Prüfung erklären sich die Gutachter nur „zu 99 Prozent“ sicher. 2014 bestätigt das Projekt Flyspeck den Beweis vollständig per Software.
5. 2022 Das Liquid Tensor Experiment prüft einen schwierigen Satz von Peter Scholze und Dustin Clausen in Lean.
6. 2024/25 KI-Systeme erreichen bei der Internationalen Mathematik-Olympiade erst Silber-, dann Goldniveau.
7. 2026 OpenAI meldet einen Beweis zum Navier-Stokes-Problem und veröffentlicht Hunderte neue Resultate.

Neu ist also nicht, dass Computer an Beweisen beteiligt sind. Neu ist, dass ein System eigenständig Fragen bearbeitet, an denen Fachleute jahrelang gescheitert sind, und das in großer Zahl.

Was ein Beweis leisten soll

Ein Beweisassistent wie Lean garantiert, dass jeder Schritt logisch korrekt ist. Er garantiert nicht, dass die formale Aussage genau das meint, was Menschen wissen wollten. Fachleute müssen deshalb prüfen, ob die übersetzte Aussage wirklich dem ursprünglichen Problem entspricht. Bei mehreren Hundert Ergebnissen ist das eine Arbeit von Monaten.

Dazu kommt eine tiefere Frage. Der Geometer William Thurston schrieb 1994 in einem viel zitierten Aufsatz, das Ziel der Mathematik sei nicht bloß, Sätze zu beweisen, sondern das menschliche Verständnis voranzubringen. Ein korrekter Beweis, den niemand versteht, beantwortet die Frage, erklärt aber nicht, warum die Antwort stimmt. Aus dieser Sorge heraus entstand die Erklärung der Fields-Medaillenträger.

Die Geschichte zeigt allerdings auch, dass neue Werkzeuge anfangs oft misstrauisch beäugt werden. Der Computerbeweis des Vierfarbensatzes galt vielen zunächst als Notlösung, heute ist er anerkannt. Wahrscheinlich wird die Mathematik auch dieses Mal Regeln finden, wie maschinelle Ergebnisse geprüft, zitiert und verstanden werden.

Was bedeutet das für Schule und Studium?

Für das Lernen ändert sich weniger, als die Schlagzeilen vermuten lassen. Wer Mathematik versteht, kann Ergebnisse einer KI prüfen, sinnvoll nachfragen und Fehler erkennen. Das gilt für die Hausaufgabe genauso wie für die Forschung. Die Grundlagen bleiben deshalb wichtig, vom Lösen von Gleichungen bis zum Verständnis, was ein Beweis überhaupt ist.

Häufige Fragen

Quellen und weiterführende Literatur

• OpenAI: Sharing AI progress in mathematics (6. Oktober 2026, englisch)
• Clay Mathematics Institute: Navier-Stokes Equation (englisch)
• Nature: Who gets credit in the AI era? OpenAI maths bombshell sparks debate (englisch)
• Scientific American: Mathematicians marvel, and grumble, at OpenAI’s trove of new results (englisch)
• William P. Thurston: On Proof and Progress in Mathematics. In: Bulletin of the American Mathematical Society 30 (1994), S. 161–177.