Vor fünf Jahren war es fast eine Kuriosität, wenn ein Sprachmodell mehrstufige Mathematikaufgaben löste. Heute geht es nicht mehr nur darum, ob es Übungen bewältigt. Die neue Frage lautet, was geschieht, wenn es auch Forschungsergebnisse hervorbringt.
Dieser Wandel ist wichtiger als jede Benchmark-Tabelle. Über Jahrhunderte waren neue Beweise ein knappes Gut: Sie konnten Monate, Jahrzehnte oder eine ganze Karriere kosten. Publikationen, Ansehen, Ausbildung und ein großer Teil der mathematischen Kultur entstanden rund um diese Schwierigkeit.
Wenn sich die Produktion von Beweisen rechnerisch skalieren lässt, verschwindet Knappheit nicht. Sie verlagert sich.
Von Übungsaufgaben zu offenen Problemen
Die jüngste Entwicklung erklärt, warum sich die Debatte so schnell verändert hat.
OpenAI veröffentlichte 2021 GSM8K, weil große Modelle bei elementaren Aufgaben mit mehreren Denkschritten noch systematisch scheiterten. Ein Jahr später erzielte Googles Minerva deutlich bessere Ergebnisse bei technischen Aufgaben aus Schule, Hochschule und quantitativen Wissenschaften.
2023 verband FunSearch ein Modell, das Programme erzeugt, mit einem automatischen Bewerter. Das System fand neue Konstruktionen für das Cap-Set-Problem und bessere Heuristiken für Bin Packing. Entscheidend war der konzeptionelle Sprung: Kandidaten konnten getestet und beibehalten werden, wenn sie den Stand der Forschung verbesserten.
2024 näherte sich AlphaGeometry auf historischen Geometrieaufgaben dem durchschnittlichen Niveau menschlicher Goldmedaillengewinner. AlphaProof und AlphaGeometry 2 lösten anschließend vier der sechs Aufgaben der Internationalen Mathematik-Olympiade: 28 von 42 Punkten, Silberniveau.
Im Juli 2025 erreichte eine fortgeschrittene Version von Gemini Deep Think Goldniveau: fünf Aufgaben, 35 Punkte und Beweise in natürlicher Sprache innerhalb des 4,5-Stunden-Limits. Die symbolische Hürde des Wettbewerbs war gefallen. Eine bequeme Unterscheidung blieb: Eine Olympiade ist keine Forschung.
2026 ändert sich die Art der Evidenz
First Proof prüfte genau diese Grenze. Das Projekt sammelte zehn Probleme aus realer Forschungsarbeit, deren Lösungen den Autoren bekannt, aber nie veröffentlicht worden waren. Vier Systeme arbeiteten unter kontrollierten Bedingungen; 30 Fachleute begutachteten die Antworten.
Bei sieben der zehn Probleme lieferte mindestens ein System eine Lösung, die als praktisch fehlerfrei oder nur geringfügig überarbeitungsbedürftig eingestuft wurde. Der Bericht dokumentiert zugleich die Schwächen: Systeme erklärten routinemäßige Teile oft ausführlich, übersprangen aber den schwierigsten Schritt; manche Quellen stützten die jeweilige Behauptung nicht.
Das ist aussagekräftiger als die Behauptung „KI kann Mathematik“. Es zeigt echte Leistungsfähigkeit in einer kleinen Stichprobe – und die Fehler, die sichtbar werden, sobald plausibler Text einer fachlichen Prüfung standhalten muss.
Im Mai veröffentlichte OpenAI ein von einem internen Modell erzeugtes Gegenbeispiel, das eine Erdős-Vermutung zu Einheitsabständen in der Ebene widerlegte. Externe Mathematiker prüften den Beweis und verfassten einen Begleitartikel, um ihn zu erklären und einzuordnen.
Im August stellte OpenAI zehn Resultate seines internen Astra-Systems aus Geometrie, Codierungstheorie, Gruppentheorie, Komplexität, Kryptografie und Kombinatorik vor. Nach Angaben des Unternehmens erzeugte das System die Argumente, Menschen bereiteten mit dem Modell die Manuskripte vor und anschließend formalisierte das Modell jedes Argument in Lean. Die Ergebnisse sind öffentlich und prüfbar; ihre langfristige Bedeutung muss jedoch die mathematische Gemeinschaft bestimmen, nicht die Ankündigung eines Unternehmens.
Wenige Tage später meldete Anthropic einen weiteren bemerkenswerten Fortschritt. Eine experimentelle Claude-Version versuchte, die Riemannsche Vermutung anzugreifen. Sie löste sie nicht. Dabei entstand jedoch ein Argument, das eine verwandte Untergrenze für den Anteil der Zeta-Nullstellen auf der kritischen Geraden von 41,6 auf 67,2 Prozent erhöht.
Das bedeutet nicht, dass die Vermutung „zu 67 Prozent gelöst“ ist. Anthropic sagt ausdrücklich, dass die Technik voraussichtlich nicht zu einem Beweis führen wird. Zwei Mathematiker des Unternehmens validierten die Arbeit, externe Fachleute untersuchten sie und eine Lean-Formalisierung liegt vor. Es ist ein Fortschritt bei einer verwandten Frage, kein Bruchteil der Hauptvermutung.
Einen Beweis prüfen heißt nicht, ihn zu verstehen
Mathematik besitzt gegenüber anderen Wissenschaften einen besonderen Vorteil. Ein von einem Modell vorgeschlagenes Molekül braucht weiterhin ein Labor. Ein Beweis kann in ein formales Objekt übersetzt und von einem kleinen Kernel Schritt für Schritt geprüft werden. Lean muss weder dem Ruf eines Unternehmens noch der Intuition eines Autors vertrauen.
Formale Verifikation beantwortet jedoch nur eine begrenzte Frage: Folgt die Schlussfolgerung aus den kodierten Axiomen und Definitionen durch gültige Inferenzen? Sie sagt nicht, ob die Formalisierung den beabsichtigten Satz trifft, ob der Beweis etwas erklärt oder ob das Ergebnis Aufmerksamkeit verdient.
Ein Beweis mit hunderttausend Zeilen kann korrekt und dennoch unbrauchbar sein, wenn die Gemeinschaft seine zentrale Idee nicht versteht. Auch flüssige Prosa genügt nicht: Eine überpolierte Erklärung kann Entscheidungen, Fehlversuche und Verbindungen verbergen, durch die Menschen ein Argument tatsächlich lernen.
Von Beweisknappheit zu Beweisverdauungsproblemen
Terence Tao beschreibt das Risiko als Übergang von knappen zu überreichlich vorhandenen Beweisen. Wenn KI einen relevanten Anteil der Forschungsaufgaben übernimmt, entsteht eine Kette von Engpässen:
- einen Beweiskandidaten erzeugen;
- seine Korrektheit prüfen;
- ihn so erklären, dass andere ihn verstehen;
- ihn durch die Gemeinschaft bewerten und nutzen lassen;
- ihn in Theorien, Lehre und Lehrbücher integrieren.
Die Automatisierung der ersten Stufe automatisiert die übrigen nicht. Sie kann sie überfluten. Beweise können sich schneller ansammeln, als wir sie begutachten, lesen und in gemeinsames Wissen verwandeln können.
Das Problem ist älter als KI. Spezialisierung, lange Arbeiten und der Druck auf das Peer Review hatten bereits eine schwer verdauliche Literatur geschaffen. Massengenerierung kann dieses Missverhältnis vervielfachen.
Vielleicht war nie nur der Satz das Wertvolle
Probleme zu lösen ist nur ein Teil mathematischer Arbeit. Gute Fragen auszuwählen, Definitionen zu entwickeln, Verbindungen zu finden, Urteilsvermögen aufzubauen, zu lehren und eine Gemeinschaft zu erhalten, gehört ebenso dazu.
Historisch waren diese Tätigkeiten miteinander korreliert. Ein schwieriger Beweis verlangte meist tiefes Verständnis; dabei entstanden Methoden, Intuitionen und neue Fragen. „Ein Ergebnis beweisen“ konnte daher als grober Stellvertreter für viele weitere Beiträge dienen.
KI kann diese Korrelation aufbrechen. Wenn die Erzeugung eines Beweises Minuten dauert, sein Verständnis aber Monate, ist das Ergebnis kein ausreichendes Maß für wertvolle Arbeit mehr.
Damit entstehen unbequemere Fragen:
- Wer erhält Anerkennung, wenn verschiedene Akteure einen Beweis erzeugen, auswählen, prüfen und erklären?
- Wie bilden wir Mathematiker aus, wenn gerade die mühsamen Lernschritte automatisiert werden?
- Wie priorisieren wir eine Literatur, die schneller wächst, als Menschen sie lesen können?
- Kann eine Theorie formal korrekt sein, ohne dass ein Mensch sie als Ganzes versteht?
- Welche Tätigkeiten sollten menschlich bleiben, auch wenn sie automatisierbar sind?
Die Antwort besteht weder darin, jede Automatisierung abzulehnen, noch alles zu akzeptieren, was einen Prüfer passiert. Wir brauchen Prozesse, in denen Erzeugung, Validierung, Zuschreibung und Erklärung getrennt und sichtbar sind.
KI macht Mathematik nicht weniger interessant. Sie macht es unmöglich, Beweisproduktion weiter mit Verständnis gleichzusetzen. Wenn das Beweisen nicht mehr der schwierige Teil ist, entdecken wir vielleicht, dass der Wert immer auch darin lag, zu wissen, was man beweisen sollte, warum es zählt und wie man es für andere verständlich macht.
Quellen
- OpenAI: GSM8K
- Google Research: Minerva
- Google DeepMind: FunSearch
- Google DeepMind: AlphaProof und AlphaGeometry 2 bei der IMO 2024
- Google DeepMind: Gemini Deep Think bei der IMO 2025
- First Proof: Bericht zur zweiten Runde
- OpenAI: Gegenbeispiel zur Einheitsabstandsvermutung
- OpenAI: zehn Fortschritte in Mathematik und theoretischer Informatik
- Anthropic: Fortschritt zur Riemannschen Zetafunktion
- Terence Tao: Mathematics in the age of AI
