AlphaProof

AlphaProof ist ein System von Google DeepMind, das mathematische Beweise im Beweisassistenten Lean erzeugt. Es lernt durch bestärkendes Lernen und erreichte bei der Internationalen Mathematik-Olympiade 2024 gemeinsam mit dem Geometriesystem AlphaGeometry 2 ein Ergebnis auf Silbermedaillenniveau. Die Methodik wurde im November 2025 in Nature veröffentlicht.

Zusammenfassung

AlphaProof überträgt das Vorgehen von AlphaZero auf die Mathematik: Statt Spielzüge sucht das System Beweisschritte, und statt eines Spielergebnisses liefert der Beweisassistent das Rückmeldesignal.

Der entscheidende Unterschied zu Sprachmodellen liegt in der Verlässlichkeit – ein von Lean akzeptierter Beweis ist im Rahmen des Axiomensystems fehlerfrei.

Bei der IMO 2024 löste das kombinierte System vier von sechs Aufgaben und erzielte 28 von 42 Punkten, darunter die schwerste Aufgabe des Wettbewerbs, die nur fünf von 609 menschlichen Teilnehmenden lösten. Die Entwicklung seither zeigt jedoch eine Verschiebung: 2025 erreichte Gemini mit dem Modus Deep Think Goldniveau in natürlicher Sprache und ohne formale Zwischenschritte.

Funktionsweise

Das System beruht auf drei Bestandteilen:

Formale Umgebung. Beweise werden in Lean formuliert und dort geprüft. Damit steht ein eindeutiges Korrektheitsurteil zur Verfügung – die Voraussetzung dafür, dass bestärkendes Lernen überhaupt möglich ist.

Autoformalisierung. Da formalisierte Aufgaben knapp sind, übersetzte ein Sprachmodell Millionen natürlichsprachlicher Aufgaben in formale Form. Aus diesem Bestand entstand der Trainingsvorrat.

Test-Time RL. Für besonders schwere Aufgaben erzeugt das System zur Antwortzeit Millionen verwandter Varianten des Problems und lernt aus ihnen – eine aufgabenspezifische Anpassung während der Lösung selbst. Der Ansatz verbindet damit Skalierung der Trainingszeit mit Skalierung der Inferenzzeit.

Die Suche folgt dem Vorbild von AlphaZero: Ein neuronales Netz schlägt Schritte vor, eine Suche vertieft aussichtsreiche Pfade, das Ergebnis des Prüfers dient als Belohnung.

Ergebnisse

Bei der IMO 2024 löste AlphaProof drei der fünf nichtgeometrischen Aufgaben – zwei aus der Algebra, eine aus der Zahlentheorie –, AlphaGeometry 2 die Geometrieaufgabe. Die beiden Kombinatorikaufgaben blieben ungelöst. Auf jeder gelösten Aufgabe erreichte das System die volle Punktzahl; die Goldschwelle lag bei 29 Punkten.

Einschränkend gilt: Die Aufgaben mussten 2024 von Menschen in formale Sprache übertragen werden, und die Rechenzeit überschritt den Wettbewerbsrahmen erheblich – für einzelne Aufgaben mehrere Tage.

Einordnung

Verlässlichkeit gegen Lesbarkeit. Der Vorzug des formalen Wegs ist die garantierte Korrektheit. Sein Preis ist die Lesbarkeit: Formale Beweise sind umfangreich und für Mathematiker ohne einschlägige Übung schwer zugänglich. Systeme, die in natürlicher Sprache arbeiten, erzeugen lesbare Beweise ohne Garantie.

Die Verschiebung von 2025. Dass Gemini mit Deep Think ein Jahr später Goldniveau in natürlicher Sprache erreichte – ohne Übersetzung durch Menschen und innerhalb der Wettbewerbszeit –, wurde als Hinweis darauf gelesen, dass der formale Umweg für Wettbewerbsaufgaben nicht zwingend ist. Google DeepMind erklärte, beide Linien weiterzuverfolgen, und sieht die Verbindung sprachlicher Gewandtheit mit geprüftem Schließen als das eigentliche Ziel.

Anschlusssysteme. Nach AlphaProof entstand eine Reihe weiterer Systeme für formale Beweisführung, darunter Aristotle von Harmonic, das bei der IMO 2025 Goldniveau erreichte, sowie mehrere quelloffene Systeme. Einzelne dieser Systeme haben Lösungen offener Erdős-Probleme in Lean formalisiert.

Kritik und Grenzen

Wettbewerbsaufgaben sind nicht Forschung. Olympiadeaufgaben haben eine bekannte Lösung, einen klaren Rahmen und eine überschaubare Länge. Forschungsprobleme haben das nicht. Die Autoren der Nature-Arbeit benennen selbst Grenzen bei anderen Formen schwieriger Aufgaben.

Rechenaufwand. Das Verfahren, zur Antwortzeit Millionen von Varianten zu erzeugen, ist außerordentlich rechenintensiv und für den Regelbetrieb nicht ohne Weiteres geeignet.

Reichweite der Formalisierung. Was sich nicht formalisieren lässt, ist dem System nicht zugänglich. Weite Bereiche der Forschungsmathematik liegen außerhalb dessen, was mathlib abdeckt.

Verstehen. Ein geprüfter Beweis erklärt nicht, warum ein Satz gilt. Terence Tao betont, dass die Erzeugung inzwischen weniger das Nadelöhr ist als das, was danach kommt – Prüfung, Darstellung und Einordnung in den Bestand des Fachs.

Warum Mathematik der günstige Fall ist

Der Erfolg des Systems beruht auf einer Eigenschaft des Gegenstands, die sich kaum auf andere Felder übertragen lässt: Formalisierte Mathematik liefert ein vollständiges, sofort verfügbares und unbestechliches Urteil darüber, ob ein Ergebnis richtig ist. Ein Beweisprüfer nimmt einen Beweis an oder nicht; ein Zwischenergebnis ist nicht ungefähr korrekt.

Damit ist die Voraussetzung erfüllt, unter der bestärkendes Lernen seine Stärke ausspielt. Das System kann beliebig viele Versuche unternehmen, jeden davon selbst bewerten und aus dem Ergebnis lernen, ohne dass ein Mensch eingreifen müsste. Genau dieselbe Konstellation liegt den Erfolgen bei Brettspielen zugrunde: geschlossene Regeln, eindeutiger Ausgang, unbegrenzt wiederholbar.

Die Felder, in denen vergleichbare Fortschritte erhofft werden – Medizin, Recht, Wirtschaftspolitik, Ingenieurwesen –, haben diese Eigenschaft nicht. Dort ist das Urteil über die Richtigkeit einer Lösung teuer, langsam, umstritten oder erst nach Jahren verfügbar. Wer aus mathematischen Erfolgen auf allgemeine Problemlösefähigkeit schließt, überträgt daher weniger eine Fähigkeit als die Verfügbarkeit eines Prüfsteins.

Ein zweiter, vorgelagerter Engpass ist die Übersetzung. Eine natürlichsprachlich gestellte Aufgabe muss zunächst in die formale Sprache überführt werden, und diese Überführung ist selbst fehleranfällig: Ein formal einwandfrei bewiesener Satz kann eine andere Aussage sein als die ursprünglich gemeinte. Die Verlässlichkeit des Gesamtsystems ist damit nicht höher als die seines am wenigsten überprüfbaren Schritts.

Verwandte Begriffe

• Lean – formale Umgebung des Systems
• Google DeepMind – Entwicklerorganisation
• AlphaGo – Vorbild des Lernverfahrens
• Formale Verifikation – zugrunde liegendes Prüfprinzip
• Gemini – Modellreihe, die den natürlichsprachlichen Weg verfolgt
• Terence Tao – Mathematiker mit einschlägiger Einordnung
• Test-Time Compute – Skalierungsachse, die das System nutzt
• Synthetische Daten – autoformalisierte Aufgaben als Trainingsvorrat

Quellenangaben

1. Chervonyi, Yuri u. a. (2025): Gold-Medalist Performance in Solving Olympiad Geometry with AlphaGeometry 2. In: Journal of Machine Learning Research 26, S. 1–39.
2. de Moura, Leonardo / Ullrich, Sebastian (2021): The Lean 4 Theorem Prover and Programming Language. In: CADE-28, LNCS 12699, S. 625–635.
3. Google DeepMind (2024): AI Achieves Silver-Medal Standard Solving International Mathematical Olympiad Problems. Juli 2024.
4. Google DeepMind (2025): Advanced Version of Gemini with Deep Think Officially Achieves Gold-Medal Standard at the International Mathematical Olympiad. Juli 2025.
5. Hubert, Thomas u. a. (Google DeepMind) (2025): Olympiad-Level Formal Mathematical Reasoning with Reinforcement Learning. In: Nature, veröffentlicht 12. November 2025. DOI: 10.1038/s41586-025-09833-y.
6. Tao, Terence (2026): Mathematics in the Age of AI. Öffentliche Vorlesung, International Congress of Mathematicians, Philadelphia, 24. Juli 2026.

← Zurück zur Lexikon-Übersicht

Zuletzt bearbeitet: 10. August 2026

Zusammengestellt, formuliert, lektoriert und korrigiert mit KI-Unterstützung. Kuratiert von Nils Brauer. Alle Angaben ohne Gewähr.