Künstliche Intelligenz rückt in der Mathematik in neue Bereiche vor. Aktuelle Sprachmodelle liefern zunehmend eigenständige Beweise zu lange offenen Problemen.
Unerwarteter Durchbruch bei Erdős-Aufgaben
Am vergangenen Wochenende testete der Softwareingenieur, frühere Quant-Forscher und Start-up-Gründer Neel Somani die mathematischen Fähigkeiten eines neuen Modells von OpenAI. Er fügte ein offenes Problem in ChatGPT ein, ließ das System 15 Minuten „nachdenken“ und fand anschließend eine vollständige Lösung vor. Somani überprüfte den Beweis und formaliserte ihn mit einem Werkzeug namens Harmonic – alles erwies sich als korrekt.
Somani wollte eigentlich nur eine Grundlage schaffen, um zu sehen, bis zu welchem Punkt große Sprachmodelle offene mathematische Probleme lösen können und wo sie an ihre Grenzen stoßen. Zu seiner Überraschung verschob das aktuelle Modell diese Grenze spürbar nach vorn.
Besonders eindrucksvoll ist die gedankliche Herleitung von ChatGPT, die mathematische Axiome wie die Formel von Legendre, das Postulat von Bertrand und den „Davidstern-Satz“ systematisch heranzieht. Schließlich stieß das Modell auf einen Beitrag auf Math Overflow aus dem Jahr 2013, in dem der Harvard-Mathematiker Noam Elkies eine elegante Lösung für ein ähnliches Problem präsentierte. Der abschließende Beweis von ChatGPT wich jedoch in wichtigen Punkten von Elkies’ Arbeit ab und lieferte eine vollständigere Lösung zu einer Variante eines Problems des legendären Mathematikers Paul Erdős, dessen umfangreiche Sammlung offener Fragen inzwischen als Testfeld für KI gilt.
GPT 5.2 und andere Werkzeuge beschleunigen die Forschung
KI-gestützte Werkzeuge sind in der Mathematik inzwischen weit verbreitet, von auf Formalisierung ausgelegten Sprachmodellen wie Aristoteles von Harmonic bis zu Literaturrecherche-Tools wie OpenAIs „Deep Research“. Seit der Veröffentlichung von GPT 5.2 – das Somani als „erfahrungsgemäß besser im mathematischen Schließen als frühere Versionen“ beschreibt – ist die Zahl der gelösten Probleme deutlich gestiegen. Das wirft neue Fragen dazu auf, inwieweit große Sprachmodelle tatsächlich die Grenzen des menschlichen Wissens verschieben können.
Somani untersuchte konkret die Erdős-Probleme, eine online gepflegte Sammlung von über tausend Vermutungen des ungarischen Mathematikers. Diese Aufgaben sind für KI-gestützte Mathematik besonders reizvoll, weil sie sich stark in Thema und Schwierigkeitsgrad unterscheiden. Die ersten autonomen Lösungen kamen bereits im November von einem Gemini-basierten Modell namens AlphaEvolve. Inzwischen zeigt sich jedoch, dass GPT 5.2 bei anspruchsvoller Mathematik besonders treffsicher agiert.
Seit Weihnachten wurden auf der Erdős-Webseite 15 Probleme von „offen“ auf „gelöst“ umgestellt, bei 11 Lösungen wird explizit der Einsatz von KI-Modellen erwähnt. Der renommierte Mathematiker Terence Tao bietet auf seiner GitHub-Seite einen differenzierteren Überblick und zählt acht Probleme, bei denen KI-Modelle eigenständig wesentliche Fortschritte erzielt haben. In sechs weiteren Fällen bestand der Beitrag darin, relevante frühere Arbeiten zu finden und weiterzuführen. Noch sind die Systeme weit davon entfernt, völlig ohne menschliche Beteiligung zu arbeiten, aber ihre Rolle in der Forschung wird zunehmend wichtiger.
Formalisierung und Akzeptanz in der Fachwelt
Auf Mastodon vermutete Tao, dass die skalierbare Natur von KI-Systemen sie besonders geeignet macht, sich systematisch der „langen Schwanzverteilung“ wenig bekannter Erdős-Probleme zu widmen, von denen viele vergleichsweise direkte Lösungen besitzen. Dadurch steigt die Wahrscheinlichkeit, dass gerade diese leichteren Aufgaben eher von rein KI-basierten Ansätzen gelöst werden als durch Menschen oder gemischte Teams.
Ein weiterer Treiber ist der Trend zur Formalisierung, also zur präzisen, maschinenlesbaren Darstellung mathematischer Beweise. Dieser Prozess erleichtert Überprüfung und Weiterentwicklung, ist aber aufwendig. Zwar braucht Formalisierung grundsätzlich weder KI noch Computer, doch neue automatisierte Werkzeuge machen die Arbeit deutlich effizienter. Der quelloffene „Beweisassistent“ Lean, 2013 bei Microsoft Research entwickelt, hat sich als Standardwerkzeug zur Formalisierung von Beweisen etabliert. KI-Tools wie Aristoteles von Harmonic versprechen zudem, große Teile dieser Arbeit zu automatisieren.
Für Harmonic-Gründer Tudor Achim ist der sprunghafte Anstieg gelöster Erdős-Probleme weniger entscheidend als die zunehmende Akzeptanz der Werkzeuge in der Spitze der Forschung. Wichtiger sei für ihn, dass Professor:innen der Mathematik und Informatik diese Tools aktiv nutzen. Diese Personen hätten einen Ruf zu verlieren, betont Achim, und wenn sie sagen, dass sie Aristoteles oder ChatGPT einsetzen, sei das ein starkes Indiz für die Relevanz der Technologie.
Via: https://techcrunch.com
Titelbild KI (Zur Illustration)
