Dennis L.
Ein neuer Mathematiktest zeigt eine Grenze moderner KI, die in normalen Benchmarks oft verborgen bleibt. Beim Projekt First Proof mussten Sprachmodelle an bisher unveröffentlichten Problemen aus der Forschungsmathematik arbeiten. Die besten Systeme fanden mehrere brauchbare Lösungen, scheiterten aber weiterhin an der Zuverlässigkeit menschlicher Spitzenmathematiker. Besonders brisant ist der Befund, weil KI erst vor Kurzem bei olympiadennahen Aufgaben deutlich stärker geworden ist.
Künstliche Intelligenz hat in den vergangenen Jahren bei mathematischen Aufgaben große Fortschritte erzielt. Besonders sichtbar wurde das bei Wettbewerbsproblemen, bei denen Aufgaben klar gestellt, Lösungen eindeutig bewertbar und viele verwandte Beispiele öffentlich verfügbar sind. Solche Tests messen wichtige Fähigkeiten, sie zeigen aber nur einen Ausschnitt mathematischen Denkens. In der echten Forschungsmathematik geht es nicht nur darum, eine elegante Rechenidee zu finden oder ein bekanntes Muster wiederzuerkennen. Ein Beweis muss neue Begriffe sinnvoll verbinden, versteckte Spezialfälle abdecken, falsche Abkürzungen vermeiden und am Ende einer fachlichen Begutachtung standhalten. Genau dort setzt der neue Mathematiktest an. Das Projekt First Proof prüft, ob moderne Sprachmodelle nicht nur Aufgaben lösen, sondern eigenständig an Problemen arbeiten können, die tatsächlich aus laufender mathematischer Forschung stammen und nicht vorher öffentlich trainierbar waren.
Die aktuellen Ergebnisse wurden am 10. Juni 2026 veröffentlicht und am Harvard Center of Mathematical Sciences and Applications vorgestellt. Laut dem First Proof Project soll der Test eine unabhängige, transparente und strenge Einschätzung der KI-Fähigkeiten in der Forschungsmathematik ermöglichen. Für die zweite Runde wurden zehn Aufgaben ausgewählt, die aus realen Forschungsprozessen stammen und anschließend von Fachgutachtern bewertet wurden. Das Harvard CMSA beschreibt den Ablauf als Blindbegutachtung, bei der menschliche Mathematiker KI-Lösungen nach wissenschaftlichen Maßstäben prüfen. Damit unterscheidet sich First Proof deutlich von vielen üblichen KI-Benchmarks, bei denen ein Modell nur die richtige Endzahl, eine kurze Begründung oder eine formal leicht prüfbare Antwort liefern muss.
Viele öffentliche KI-Tests verwenden Aufgaben, deren Struktur für große Sprachmodelle günstig ist. Die Modelle können auf bekannte Lösungsformen, ähnliche Beispiele aus Trainingsdaten oder oft wiederholte Wettbewerbsstrategien zurückgreifen. First Proof soll genau diese Abkürzung erschweren. Die Aufgaben waren vor der Veröffentlichung nicht öffentlich zugänglich und wurden so ausgewählt, dass sie mehrere mathematische Teilgebiete abdecken. Dadurch muss ein Modell nicht nur rechnen, sondern eine tragfähige Argumentation entwickeln. Ein Lösungsversuch kann sprachlich überzeugend sein und trotzdem an einer kleinen Lücke scheitern, die den gesamten Beweis unbrauchbar macht. Gerade diese Lücken sind für Laien kaum erkennbar, in der Forschungsmathematik aber entscheidend. Der Mathematiktest misst deshalb weniger, ob KI intelligent formuliert, sondern ob sie eine Aussage so begründet, dass Experten sie nach strengen Fachregeln akzeptieren können.
Die Ergebnisse zeigen ein gemischtes Bild. Die besten eingesetzten Systeme konnten mehrere der zehn Probleme im Wesentlichen richtig lösen oder so weit bearbeiten, dass nur kleinere Korrekturen nötig waren. Gleichzeitig blieb kein Modell auf dem Niveau einer verlässlich arbeitenden Gruppe menschlicher Experten. Einige Lösungen enthielten fehlende Belege, problematische Literaturverweise oder argumentativ starke, aber mathematisch nicht ausreichend abgesicherte Passagen. Das macht den Befund spannender als ein einfaches Scheitern. Künstliche Intelligenz ist in diesem Bereich nicht mehr bloß ein Spielzeug für Standardaufgaben, aber sie ist auch kein Ersatz für fachliche Kontrolle. Der Test zeigt damit eine Zwischenstufe: Sprachmodelle können Forscher bei Ideen, Literatur, Varianten und langen Rechenwegen unterstützen, doch die eigentliche Qualitätssicherung bleibt weiterhin eine menschliche Aufgabe.
Mathematik unterscheidet sich von vielen anderen Wissensfeldern, weil eine Lösung nicht nur wahrscheinlich oder nützlich sein darf. Sie muss logisch zwingend sein. Ein einzelner fehlerhafter Übergang kann aus einer scheinbar starken Herleitung eine falsche Behauptung machen. Genau deshalb ist die Leistung menschlicher Mathematiker im First Proof Test so wichtig. Sie beurteilen nicht nur, ob das Ergebnis plausibel klingt, sondern ob jeder entscheidende Schritt trägt. Der neue Benchmark macht sichtbar, dass Sprachmodelle vor allem dort Probleme bekommen, wo ein Beweis nicht aus bekannten Mustern zusammengesetzt werden kann. Sie können lange Argumentationsketten erzeugen, aber sie kontrollieren deren Gültigkeit nicht immer mit derselben Strenge wie ein erfahrener Fachgutachter. Für die Forschung ist das ein praktisches Problem, weil eine beeindruckend formulierte falsche Lösung mehr Prüfaufwand erzeugen kann als gar keine Lösung.
Gleichzeitig wäre es falsch, die Ergebnisse als reine Niederlage für Künstliche Intelligenz zu lesen. Mehrere Lösungen kamen nahe genug an akzeptable Beweise heran, um als ernstzunehmende Beiträge zur Forschungspraxis zu gelten. Besonders stark sind die Systeme, wenn sie Literatur durchsuchen, ungewöhnliche Ansätze kombinieren oder ermüdende Varianten systematisch verfolgen. Diese Fähigkeit kann menschliche Forschung beschleunigen, wenn die Resultate streng überprüft werden. Der entscheidende Punkt ist die Rollenverteilung. OpenAI und andere Gruppen zeigen mit solchen Tests, dass KI im mathematischen Arbeiten an Relevanz gewinnt, doch First Proof zeigt zugleich, dass der wichtigste Maßstab nicht eine spektakuläre Einzelleistung ist. Entscheidend ist, ob ein System regelmäßig korrekte, nachvollziehbare und sauber belegte Lösungen liefert. Genau daran scheitern die besten Modelle noch zu oft.
Der neue Mathematiktest ist auch deshalb relevant, weil er eine verbreitete Erzählung über KI korrigiert. Wenn ein Modell bei einzelnen Olympiadeaufgaben oder berühmten Problemen beeindruckende Ergebnisse erzielt, entsteht schnell der Eindruck, mathematische Forschung stehe kurz vor der vollständigen Automatisierung. First Proof zeigt ein nüchterneres Bild. Fortschritt ist klar vorhanden, aber er verteilt sich ungleich. Modelle können in einzelnen Aufgaben sehr stark sein und in anderen an scheinbar kleinen Details scheitern. Dieses Muster ist typisch für heutige Sprachmodelle, die enorme Mengen an Text, Code und mathematischen Darstellungen verarbeiten, aber keine menschliche Intuition im eigentlichen Sinn besitzen. Sie erzeugen Lösungskandidaten und bewerten Wahrscheinlichkeiten, während Mathematiker Begriffe, Beweislücken und methodische Grenzen in einem tieferen fachlichen Zusammenhang prüfen.
Für die Technikentwicklung ist der Befund trotzdem wertvoll. Er zeigt, welche Art von KI-Systemen künftig gebraucht wird: nicht nur größere Sprachmodelle, sondern Werkzeuge, die Beweise formal prüfen, Quellen korrekt zuordnen und Fehler früh erkennen. In der Forschungsmathematik könnte daraus ein Arbeitsmodell entstehen, bei dem KI schnelle Entwürfe liefert, formale Prüfsysteme die logische Konsistenz testen und menschliche Mathematiker die eigentliche wissenschaftliche Bedeutung einordnen. Der Mathematiktest macht damit keine einfache Aussage nach dem Muster Mensch gegen Maschine. Er zeigt genauer, an welcher Stelle die Maschine stark ist und wo der Mensch unverzichtbar bleibt. Gerade deshalb ist First Proof ein wichtiger Nachrichtenbefund für die KI-Forschung: Der Abstand wird kleiner, aber er verschwindet nicht dort, wo mathematische Wahrheit vollständig bewiesen werden muss.