Die Mathematik erlebt derzeit einen beispiellosen Wandel durch den Einsatz moderner KI-Modelle. Während Resultat-Durchbrüche von Frontier-Modellen bisher meist in geschlossenen Forschungslaboren stattfanden, fällt nun eine jahrzehntealte Festung der reinen Mathematik im Open-Source-Bereich: Zahlreiche offene Rätsel des legendenumwobenen Mathematikers Paul Erdős werden in rascher Folge von KI-Systemen gelöst und formal verifiziert.
Besonders die Arbeit des Forschers Shouqiao Wang sorgt in der internationalen Mathematik- und KI-Community für Aufsehen. Mit einem speziellen Codex-Workflow, der auf GPT-5.6 basiert, gelang ihm und seinem Forschungspartner Davide Crapis unter anderem der vollständige Beweis für das Erdős-Problem 690. Auf seinem GitHub-Repository sammelt Wang inzwischen eine wachsende Serie von Lösungen für bisher ungelöste Probleme aus Erdős' umfangreichem Nachlass.
Vom mathematischen Entwurf zur unerbittlichen Lean-4-Verifikation
Ein zentrales Problem KI-generierter Beweise war bisher die Gefahr von Halluzinationen. KI-Modelle erzeugen zwar oft brillante Beweisideen, neigen in feinen logischen Zwischenschritten jedoch zu subtilen Trugschlüssen. Um dieses Problem zu lösen, setzt die neue Generation von Forscherinnen und Forschern auf die formale Beweisprüfung in der Sprachumgebung Lean 4.
In dieser Arbeitsweise entwirft das KI-Modell zunächst den mathematischen Beweis in natürlicher Sprache oder TeX. Anschließend wird der Beweis Schritt für Schritt in maschinenlesbare Lean-4-Terme übersetzt. Der Lean-Compiler prüft jede logische Deduktion ohne menschliche Voreingenommenheit. Wenn der Code fehlerfrei durch den Compiler läuft, gilt der Beweis als mathematisch unumstößlich garantiert. Nach ersten Durchbrüchen bei der Widerlegung einer Geometrie-Vermutung und den Erfolgen von DeepMind und OpenAI bei den Erdős-Rätseln zeigt die Arbeit an Open-Source-Modellen, dass dieser Ansatz nun breiten Zugang findet.
Erdős-Erbe als Härtetest für Künstliche Intelligenz
Paul Erdős (1913-1996) galt als einer der produktivsten Mathematiker der Geschichte. Er hinterließ der Weltgemeinschaft hunderte offene Aufgabenstellungen aus Zahlentheorie, Graphentheorie und Kombinatorik, auf deren Lösung er oft Preisgelder von 25 bis 10.000 Dollar auslobte. Während menschliche Mathematiker über Generationen hinweg mühsam einzelne Erdős-Kopfnüsse knackten, führt der Verbund aus Large Language Models und automatisierten Beweisassistenten zu einer völlig neuen Lösungsgeschwindigkeit.
Wie Wang in Dokumentationen zu seinem Projekt beschreibt, erfordere die Erarbeitung formaler Beweise mit KI-Unterstützung nicht zwingend jahrzehntelange Spezialisierung auf dem jeweiligen Teilgebiet. Vielmehr kombiniere der Arbeitsablauf die strategische Formulierungskompetenz des Menschen mit der enormen Such- und Formalisierungskapazität des KI-Agenten. Dies unterstreicht auch die Dynamik, die bei aktuellen Benchmarks wie FrontierMath und offenen mathematischen Problemen beobachtet wird.
🎯 Was das für die Praxis bedeutet
1. Formale Verifikation als Sicherheitsstandard: Die Kombination aus generativer KI und strengen Prüfsystemen wie Lean zeigt, wie Halluzinationen in kritischen Domänen wie Softwareentwicklung und Wissenschaft wirksam eliminiert werden.
2. Demokratisierung wissenschaftlicher Entdeckungen: Durch KI-gestützte Workflows verschiebt sich der Fokus von reinem Handwerk und manueller Rechenarbeit auf die richtige Formulierung und Führung des KI-Agenten.
3. Beschleunigter Wissenstransfer: Komplexe mathematische Erkenntnisse lassen sich durch maschinenlesbaren Code schneller in praxistaugliche Algorithmen für Kryptografie, Optimierung und Datenanalyse überführen.
