KI knackt Mathematikprobleme. Was zählt als Beweis?

Nimm eine nichtnegative ganze Zahl n. Rechne n² + n + 41. Für n = 0 bekommst du 41, für 1 die 43, für 2 die 47. Alles Primzahlen: Zahlen größer als 1, die nur durch 1 und sich selbst teilbar sind. Das sieht nach einer praktischen Primzahlmaschine aus. Würdest du wetten, dass die Formel immer funktioniert?

Für n = 40 steht da 1.600 + 40 + 41 = 1.681 = 41 × 41. Eine einzige Zahl zerstört die Behauptung „immer eine Primzahl“. Unsere ersten drei Tests waren korrekt. Die Schlussfolgerung war zu groß. Dieses vollständig ausgerechnete Lehrbeispiel ist der Schlüssel zur aktuellen Mathematik-Geschichte: Eine überzeugende Folge von Treffern und ein Beweis beantworten verschiedene Fragen.

Am 8. September 2026 veröffentlichte OpenAI eine angekündigte Lösung zum Navier–Stokes-Problem: eine analytische Arbeit und eine formalisierte Fassung. Das verwendete interne KI-System war laut Anbieter leistungsfähiger als das öffentlich angebotene GPT-6 Astra. Ankündigung und Versuchsaufbau.

Navier–Stokes-Gleichungen beschreiben Bewegung von Flüssigkeiten. Ein schwieriger Teil ist das Zusammenspiel: Die Bewegung transportiert sich selbst weiter; Viskosität glättet Unterschiede. Können sich anfangs glatte Verhältnisse dennoch so zuspitzen, dass das mathematische Modell in endlicher Zeit zusammenbricht? Ein paar berechnete Strömungen würden diese Frage für alle zulässigen Fälle nicht entscheiden. Problemformulierung des Clay Mathematics Institute.

Die veröffentlichte Arbeit konstruiert einen Fall mit glatter äußerer Kraft: Die Flüssigkeit startet in Ruhe, die Geschwindigkeit wird im Modell innerhalb endlicher Zeit unbeschränkt, die kinetische Energie bleibt beschränkt. Das betrifft die Varianten C und D der offiziellen Aufgabe. Die Aussage ist dadurch präziser als „KI hat Turbulenz verstanden“. Sie ist auch keine Behauptung, dass reales Wasser unendlich schnell wird. Arbeit, Einleitung und Satz 1.1, formalisierte Ergebnisse.

Lass in der Erklärung die äußere Kraft weg, und du erzählst eine andere Aufgabe. Eine Simulation kann einen interessanten Kandidaten zeigen; der Nachweis muss zusätzlich die geforderten Bedingungen einhalten. Gerade bei einem großen Ergebnis sind diese Bedingungen Teil dessen, was es bedeutet.

Zurück zu etwas, das wir selbst nachrechnen können. Die Aussage lautet jetzt: Der Unterschied zwischen zwei aufeinanderfolgenden Quadratzahlen ist immer ungerade. Für 2² und 3² beträgt er 5. Für 3² und 4² beträgt er 7. Wieder könnten wir lange Beispiele sammeln.

Diesmal gibt es einen kurzen allgemeinen Grund: (n + 1)² − n² = n² + 2n + 1 − n² = 2n + 1. Für jede nichtnegative ganze Zahl n ist 2n gerade; plus 1 macht die Zahl ungerade. Die Rechnung umfasst alle n der genannten Menge. In einer Zeichnung wird aus einem n-mal-n-Quadrat ein größeres Quadrat, indem eine L-förmige Schicht aus n + n + 1 Kästchen dazukommt.

Unsere Primzahlformel lieferte getestete Beispiele und ein Gegenbeispiel. Die Quadratrechnung liefert einen allgemeinen Beweis. Beide sind viel kleiner als Navier–Stokes. Genau deshalb kann man hier den Unterschied sehen, ohne der Autorität eines Modells vertrauen zu müssen.

Lean ist ein Beweisassistent. Er wird gebraucht, um eine mathematische Aussage und ihre Begründung in einer formalen Sprache zu prüfen. Er bekommt Definitionen, Voraussetzungen, die genaue Behauptung und einen konstruierten Beweis. Sein Prüfkern kontrolliert, ob dieser Beweis die Behauptung nach den Regeln des Systems tatsächlich trägt. Heraus kommt ein akzeptierter formaler Beweis — oder eine Stelle, an der die Prüfung scheitert. Lean: Aussagen und Beweise.

Das hilft auch bei KI: Sie kann neue Wege vorschlagen und Beweisschritte ausarbeiten; die entscheidende Prüffrage wird nicht durch die flüssigste Formulierung gewonnen. Menschen müssen weiterhin prüfen, ob die formal aufgeschriebene Aussage die beabsichtigte Aufgabe beschreibt, welche Voraussetzungen und Axiome verwendet werden und wie sich der Beweis einordnen lässt. Ein korrekt bewiesener Satz über das falsche Problem löst deine ursprüngliche Frage nicht.

Am 6. Oktober 2026 stellte OpenAI weitere mathematische Ergebnisse öffentlich vor. Veröffentlichung. Das verlinkte Mathematik-Repository unterscheidet ausdrücklich verschiedene Prüfstände: Nicht alle Ergebnisse sind formalisiert; bei nicht formalisierten Arbeiten können noch Probleme auftauchen. Eine Sammlung von Manuskripten ist deshalb keine Liste gleich stark abgesicherter, unabhängig bestätigter Lösungen.

Für ein bestimmtes Ergebnis kannst du drei Dinge auseinanderhalten: Welche genaue Aussage wird beansprucht? Welcher Nachweis ist verfügbar? Wer hat welche Prüfung wirklich durchgeführt? Ein lesbarer Fachtext, ein formal prüfbares Artefakt und fachliche Begutachtung liefern unterschiedliche Informationen. In diesem Beitrag erklären wir diese Ebenen; wir behaupten keine eigene vollständige Überprüfung des großen Strömungsbeweises.

Bei einer Prüfung stehen Aufgaben und richtige Antworten vorher fest. In der Forschung musst du oft erst eine produktive Frage, einen Ansatz oder ein Gegenbeispiel finden. Ein überprüfbares neues Resultat wäre deshalb eine andere Art von Fortschritt als eine höhere Testpunktzahl. Die Besonderheit liegt auch im Anschluss: Andere können den Nachweis untersuchen, ausbauen oder einen Fehler lokalisieren.

Wenn die nächste Schlagzeile sagt, eine KI habe Mathematik geknackt, geh denselben kleinen Weg wie bei unserer Formel: Behauptung aufschreiben, Bedingungen mitnehmen, Nachweis öffnen. Frage bei einem Test nach der getesteten Menge; bei einem Gegenbeispiel nach einem konkreten Widerspruch; bei einem Beweis nach dem allgemeinen Grund. Das macht das Ergebnis verständlicher und seinen möglichen Wert genauer sichtbar.