OpenAI präsentiert einen Durchbruch: Eine interne Version des zukünftigen Astra-Modells hat zehn mathematische und theoretische Informatik-Probleme gelöst, bei denen die Forschung über mindestens zehn Jahre stagniert hatte. Die Lösungen wurden mit Lean-4-Formalisierungen transparent im Repository veröffentlicht, zusammen mit ausführlichem Paper und LLM-generierten Erklärungen der Beweisschritte. Das Ergebnis schlägt Wellen unter Mathematikern – ähnlich wie Deepblue in den 1990ern weckt es sowohl Hoffnung als auch existenzielle Fragen zur Zukunft der mathematischen Forschung. Terence Tao sieht darin den Katalysator für ein neues Modell: \"Big Mathematics\" mit dezentraler Zusammenarbeit zwischen Menschen (Kreativität) und KI (technische Arbeit).
