Laut Tests eines Softwareentwicklers und ehemaligen Quantenforschers zeigte das neueste Modell von OpenAI eine unerwartete Fähigkeit zur Lösung anspruchsvoller mathematischer Probleme Neel Somani. Somani beobachtete, dass das Modell nach 15 Minuten Bearbeitung eines Problems in ChatGPT eine vollständige Lösung generierte und anschließend den Beweis mit dem Harmonic-Tool formalisierte, was seine Genauigkeit bestätigte. Er erklärte, sein Ziel sei es, eine Grundlage für die Fähigkeit großer Sprachmodelle (LLMs) zur Lösung offener mathematischer Probleme zu schaffen. Die Gedankenkette des Modells berief sich auf mathematische Axiome, darunter die Formel von Legendre, das Postulat von Bertrand und den Satz des Davidsterns. Es wurde ein Math Overflow-Beitrag des Harvard-Mathematikers Noam Elkies aus dem Jahr 2013 gefunden, der die Lösung eines ähnlichen Problems bot, der endgültige Beweis von ChatGPT war jedoch anders und lieferte eine vollständigere Lösung für eine Version eines Problems des Mathematikers Paul Erdős. Seit der Veröffentlichung von GPT 5.2, das Somani als „anekdotisch geschickter im mathematischen Denken als frühere Iterationen“ beschrieb, hat eine wachsende Menge gelöster Probleme Fragen zur Fähigkeit von LLMs aufgeworfen, menschliches Wissen zu verbessern. Somani konzentrierte sich auf die Erdős-Probleme, eine Sammlung von über 1.000 online gepflegten Vermutungen, die sich in Thema und Schwierigkeitsgrad unterscheiden. Die ersten autonomen Lösungen für diese Probleme entstanden im November mit AlphaEvolve, einem Gemini-Modell. In jüngerer Zeit haben Somani und andere festgestellt, dass GPT 5.2 sich mit Mathematik auf hohem Niveau auskennt. Seit Dezember haben sich 15 Probleme auf der Erdős-Website von „offen“ zu „gelöst“ verschoben, wobei 11 Lösungen KI-Modellen zugeschrieben werden. Der Mathematiker Terence Tao, auf seinem GitHub-Seitestellte acht Probleme fest, bei denen KI-Modelle bedeutende autonome Fortschritte machten, und sechs Fälle, bei denen Fortschritte darin bestanden, frühere Forschungsergebnisse zu lokalisieren und darauf aufzubauen. Tao vermutete gegenüber Mastodon, dass KI-Systeme aufgrund ihrer Skalierbarkeit „besser dafür geeignet sind, systematisch auf den ‚langen Schwanz‘ obskurer Erdős-Probleme angewendet zu werden, von denen viele tatsächlich einfache Lösungen haben“, und fügte hinzu, dass „viele dieser einfacheren Erdős-Probleme jetzt eher mit rein KI-basierten Methoden als mit menschlichen oder hybriden Mitteln gelöst werden können.“ Eine treibende Kraft bei diesem Fortschritt ist die Verlagerung hin zur Formalisierung, einem arbeitsintensiven Prozess zur Überprüfung und Erweiterung mathematischer Überlegungen. Obwohl keine KI erforderlich ist, haben neue automatisierte Tools diesen Prozess vereinfacht. Der Open-Source-Beweisassistent Lean, der 2013 bei Microsoft Research entwickelt wurde, hat breite Anwendung für die Formalisierung von Beweisen gefunden, und KI-Tools wie Harmonics Aristotle zielen darauf ab, einen Großteil dieser Arbeit zu automatisieren. Tudor Achim, der Gründer von Harmonic, erklärte, dass die Beschäftigung von Mathematikern und Informatikprofessoren mit KI-Tools wichtiger sei als die Anzahl der gelösten Erdős-Probleme. Achim sagte: „Diese Leute müssen ihren Ruf schützen. Wenn sie also sagen, dass sie Aristoteles oder ChatGPT verwenden, ist das ein echter Beweis.“
