2026年7月15日，Reddit 数学板块出现了一条帖子，标题平淡无奇——大意是”看了 OpenAI 那个 CDC 猜想的证明方法后，我用 GPT-5.6 试了试，关掉了一个 30 年的缺口”。
Am 15. Juli 2026 tauchte in der Mathematik-Sektion von Reddit ein Beitrag mit unscheinbarem Titel auf — sinngemäß: „Nachdem ich mir OpenAIs Beweis der CDC-Vermutung angesehen hatte, habe ich es mit GPT-5.6 probiert und eine 30 Jahre alte Lücke geschlossen.“
Drei Tage später erreichte der Beitrag auf Hacker News 477 Upvotes und 308 Kommentare. Die Mathematiker, die den Lean-Code Zeile für Zeile gelesen hatten, waren sich auffällig einig: Diesmal handelt es sich um einen echten mathematischen Beitrag.
Nachdem der Autor die Diskussionen durchgelesen hatte, lag die eigentliche Sprengkraft darin, dass hier eine Aufgabe angegangen wurde, die selbst Mathematiker für besonders heikel halten — das Beweisen einer unteren Schranke. Und GPT-5.6 erledigte das mit einem einzigen Prompt und in 148 Minuten.
Was passierte: ein Prompt, 148 Minuten, eine 30 Jahre alte Lücke
Phillip Kerger ist Assistenzprofessor für angewandte Mathematik an der UC Berkeley, promovierte in Optimierungstheorie an der Johns Hopkins und forschte zuvor im Quanten-KI-Labor der NASA. Seit dem vergangenen Jahr arbeitete er immer wieder an einem Problem — einer seit 1996 ungelösten Komplexitätslücke im Bereich der konvexen Optimierung.
Kurz gesagt: 1996 entwarf jemand einen Algorithmus mit einer Komplexität von \\(O(d^2 \log^2 d)\\) . Allgemein war klar, dass es nicht besser als \\(O(d)\\) gehen kann (man muss schließlich jede Dimension zumindest einmal betrachten). Aber die 30 Jahre lange Lücke zwischen \\(O(d)\\) und \\(O(d^2 \log^2 d)\\) konnte niemand schließen — ist es noch schneller möglich, oder hat der alte Algorithmus sein Maximum bereits erreicht?
Kerger hatte zuvor GPT-5.4 und GPT-5.5 ausprobiert, beide scheiterten. Selbst wenn er den Ansatz manuell in die richtige Funktionsfamilie lenkte, vervollständigte das Modell die letzten Schritte nicht.
Dann kam GPT-5.6.
In Anlehnung an die Struktur des „Cyclic Double Cover“-Beweis-Prompts, den OpenAI vor einigen Wochen veröffentlicht hatte, verfasste er einen etwa zehnseitigen Prompt — mit der mathematischen Setup, einer Auflistung machbarer Beweiswege, seinen Erfahrungen aus früheren gescheiterten Versuchen und einer klaren Definition dessen, was als gültige Lösung gilt. Zunächst ließ er sich von GPT-5.6 bei der Literaturarbeit und dem Argumentationsgerüst helfen, dann fütterte er das Modell in einer durchgehenden Sitzung mit der Endversion.
148 Minuten später spuckte GPT-5.6 die vollständige Beweiskonstruktion aus.
- Bildquelle: Unsplash / GuerrillaBuzz — Illustration der Konvergenz konvexer Optimierungsmethoden. Was GPT-5.6 bewies, ist, dass die untere Kurve nicht weiter gedrückt werden kann — der Algorithmus von 1996 liegt bereits an der theoretischen Grenze. *
Das Ergebnis: Eine untere Schranke von \\(\Omega(d^2 / \log(d+1))\\), die von der bekannten oberen Schranke \\(O(d^2 \log^2 d)\\) nur noch durch einen logarithmischen Faktor abweicht. Das schließt die Möglichkeit aus, dass es einen deutlich schnelleren Ansatz als den 30 Jahre alten Algorithmus gibt.
Warum „untere Schranke beweisen“ so viel schwerer ist: ein Lauf-Vergleich
Um das Gewicht dieser Leistung zu verstehen, ein Alltagsvergleich.
Eine obere Schranke zu beweisen ist wie zu beweisen, dass Sie 100 Meter laufen können — Sie laufen einmal, drücken die Stoppuhr, fertig.
Eine untere Schranke zu beweisen ist wie zu beweisen, dass Sie unmöglich schneller laufen können — dafür müssen Sie alle denkbaren Trainingsmethoden ausschließen. Andere Schuhe? Nutzlos. Besserer Start? Nutzlos. Spezialdiät? Immer noch nutzlos. Damit „Sie können nicht unter 9 Sekunden laufen“ gilt, müssen Sie jede vorstellbare Möglichkeit durchgehen und einzeln zeigen, dass keine davon hilft.
In der Mathematik ist das Beweisen einer oberen Schranke („Ich habe eine Methode gefunden, die mindestens dieses Niveau erreicht“) relativ einfach — Sie geben einen Algorithmus an, rechnen seine Komplexität aus, fertig. Aber das Beweisen einer unteren Schranke („Es gibt keine Methode, die schneller als das hier ist“) erfordert, alle möglichen Algorithmen einzuschränken. Sie müssen zeigen: Egal wie jemand einen neuen Algorithmus entwirft, egal welchen Trick er verwendet, egal wie viele Umwege — alles nutzlos, die Grenze ist hier.
Deshalb schrieb ein Kommentator auf HN namens alternator — der sich als jemand vorstellte, der „ein bisschen Ahnung von dem Gebiet“ hat:
“Proving upper bounds is easy, it’s just how long your algorithm took. Proving non-trivial lower bounds is much harder because it requires you to constrain all possible algorithms.”
Und genau das hat GPT-5.6 diesmal getan. Es bewies nicht nur, dass Kerger konstruierte Algorithmus gut funktioniert — es bewies, dass der alte Ansatz von 1996 das theoretische Deckengelände erreicht hat. 30 Jahre lang konnte niemand die Möglichkeit ausschließen, dass „es vielleicht doch einen besseren Weg gibt“; GPT-5.6 schloss das in 148 Minuten aus.
Zwei Arten, wie KI Mathematik betreibt: nicht verwechseln
Beim Thema KI und Mathematik muss man zwei Dinge unterscheiden. Sie sehen ähnlich aus, sind aber grundverschieden.
Erste Art: KI-gestütztes Vermuten. Das passiert bereits seit Jahren. Forscher lassen Modelle nach Mustern zwischen bekannten Ergebnissen suchen und „vielversprechende“ Vermutungen erzeugen, die dann ein Mensch verifiziert. Das Modell sagt „ich glaube, diese Ungleichung könnte gelten“, und ein Mensch prüft das mit Papier und Stift oder dem Computer. In diesem Szenario ist die KI ein kluger Assistent, aber die letzte Entscheidung liegt beim Menschen.
Zweite Art: KI erbringt eigenständig einen strengen Beweis — und besteht die formale Verifikation. Das ist das, was GPT-5.6 diesmal tat. Das Modell gab nicht nur ein „plausibel klingendes“ Argument aus, sondern dieser Beweis wurde vollständig nach Lean 4 — einem mathematischen Beweisassistenten — übersetzt and Zeile für Zeile kompiliert. Lean akzeptiert keine Formulierungen wie „folgt offensichtlich“ oder „leicht einzusehen“. In Leans Welt gibt es kein Mittelding: Entweder jeder Schritt ist logisch wasserdicht, oder es gibt einen Fehler.
Kerger stellte den gesamten Lean-Code auf GitHub. Wer auch immer den Versionmanager elan installiert, das Repository klont und lake build ausführt, kann mit eigenen Augen sehen, dass der Compiler von Anfang bis Ende keine Fehler meldet. Ein zusätzliches #print axioms bestätigt das Fehlen von sorryAx (der Platzhalter in Lean für „diesen Schritt habe ich noch nicht bewiesen“) — das bedeutet, in der gesamten logischen Kette klafft keine Lücke.
Kerger veröffentlichte sein 36-seitiges Preprint, den vollständigen Prompt, den Modell-Dialog, den Lean-Code und die Build-Anleitung — alles öffentlich. Dieser Offenlegungsstandard liegt um Längen über dem mancher Papers, die KI-Unterstützung nur in einer Dankeszeile erwähnen.
- Bildquelle: Unsplash / Bozhin Karaivanov — Code-Oberfläche des Lean-Beweisassistenten. GPT-5.6 Beweis wurde vollständig nach Lean 4 übersetzt und kompiliert, in der gesamten logischen Kette gibt es kein einziges
sorry(unbewiesener Schritt). *
Fair gesagt: kritische Stimmen verdienen Gehör
Der Autor will diesen Text nicht als „KI demütigt die Menschheit“-Story verfasst. Auf r/math und HN gab es durchaus vernünftige Zweifel, und diese Stimmen sind wichtig, um das Gesamtbild zu verstehen.
Erstens, das Gebiet ist recht niche. Mehrere Kommentatoren wiesen darauf hin, dass diese untere Schranke in der konvexen Optimierung bei weitem nicht so bekannt ist wie OpenAIs zuvor gelöste „Cyclic Double Cover“-Vermutung. Letztere ist ein seit 50 Jahren offenes Problem der Graphentheorie, während die untere Schranke vor allem in einem relativ kleinen Kreis der Optimierungstheorie diskutiert wird. Ihr akademischer Wert ist echt, aber das „Ausbrechen über die Fachgrenzen hinaus“ ist begrenzt.
Zweitens, Übertragbarkeit fraglich. Die für untere Schranken nötige Denkweise — alle möglichen Algorithmen einzuschränken — ist in der Tat eine sehr schwierige Kategorie, und GPT-5.6 zeigte hier Fähigkeiten. Aber lässt sich diese Fähigkeit von der konvexen Optimierung auf andere mathematische Zweige übertragen? Das weiß bisher niemand.
Drittens, Prioritätsstreit. In der r/math-Diskussion wühlten einige in russischsprachiger Optimierungsliteratur aus den 1990er Jahren und vermuteten, dass das zentrale Lemma in Kerger Beweis möglicherweise bereits von sowjetischen Mathematikern veröffentlicht wurde — nur in Zeitschriften, die von westlichen Datenbanken selten erfasst werden. Sollte sich das bestätigen, wäre GPT-5.6 Beitrag: „Einen Beweis aus fast vergessener Literatur rekonstruiert und auf eine Weise formalisiert, die noch nie jemand genutzt hat.“ Das sind zwei unterschiedlich schwere Beiträge.
Viertens, „148 Minuten“ ist nicht die ganze Geschichte. Kerger arbeitete bereits ein Jahr lang immer wieder an diesem Problem. In dem zehnseitigen Prompt steckten sein Verständnis des Problems, gescheiterte Versuche und ausgeschlossene Sackgassen. Vor GPT-5.6 scheiterten GPT-5.4 und GPT-5.5 an derselben Aufgabe. Die 148 Minuten waren die letzte ununterbrochene Beweissuche — kein Zauber aus dem Nichts. Wie RuntimeWire berichtete: „Im Prompt steckt ein Jahr Arbeit im Fachgebiet.“
- Bildquelle: RuntimeWire / Gemini — KI-generierte Illustration des mathematischen Beweisprozesses. Es lohnt sich zu erinnern: Hinter dem Prompt steht ein Jahr fachlicher Akkumulation, die 148 Minuten sind nur die Suchzeit des letzten Schritts. *
Worauf es wirklich ankommt: dieses Arbeitsmodell
Lassen wir die Kontroversen beiseite — das Interessanteste an dieser Sache ist für den Autor nicht das konkrete Theorem.
Das Dreieck Mensch + KI + formale Verifikation hat sich als reproduzierbar erwiesen.
Kerger Vorgehen ist klar: Große Probleme in kleine Lemmata zerlegen, jedes Lemma zunächst in die strengen Formulierungen von Lean übersetzen and dann das Modell den Beweis füllen lassen. Welches Lemma nicht kompiliert, wird isoliert iteriert — eine Änderung an einer Stelle stürzt nicht den ganzen Beweis um. Dieser Prozess erfordert keinen Fields-Medaillen-Träger; die Hürde liegt darin, dass Sie Ihr Problem präzise definieren können müssen.
Mit anderen Worten: Auf dem Weg, „mittelschwere“ mathematische Probleme zu bewältigen, hat die KI nun ein operatives Rezept. Das macht Mathematiker nicht arbeitslos — Probleme definieren, Prompts konstruieren, beurteilen, ob die Ausgabe Unsinn ist: Das müssen vorerst weiter Menschen tun. Aber es verändert den Alltag der mathematischen Forschung: Forscher werden immer mehr zu Regisseuren, die KI immer mehr zum ausführenden Team.
Ein HN-Kommentator brachte es auf den Punkt: Manchmal fühlt sich diese Diskussion wie Hieroglyphen lesen an. Aber lassen Sie sich nicht von der Terminologie einschüchtern — das Wesen der Sache ist einfach. 30 Jahre lang wussten Menschen, wie schnell ein Algorithmus laufen kann, trauten sich aber nicht zu sagen „das ist das Limit“. Eine KI, geführt von einem Menschen mit einem Jahr Akkumulation, bewies in 148 Minuten „das ist das Limit“. Und dann prüfte eine andere Maschine namens Lean Hausaufgaben Zeile für Zeile und bestätigte, dass keine Abkürzung genommen wurde.
Das ist die mathematische Front im Jahr 2026 — Menschen, KI und Beweis-Compiler beginnen, in einem Projektteam zusammenzuarbeiten.
Referenzen:
- Reddit r/math: After OpenAI’s CDC proof announcement, GPT-5.6 used a prompt to close a 30-year gap in convex optimization
- HN Diskussion (item?id=48957779)
