Forschung Astra löst zehn offene Mathe-Probleme - 1. August
OpenAI veröffentlicht zehn Fortschritte aus Mathematik und theoretischer Informatik, erzeugt vom noch unveröffentlichten Modell Astra. Jedes Problem war seit mindestens zehn Jahren ungelöst - darunter die Konstruktion einer nicht-sofischen Gruppe, eine Frage, die Michail Gromow 1999 aufwarf. Alle Beweise sind in Lean 4 formalisiert und maschinell nachprüfbar (auf GitHub, Apache 2.0, „sorry"-Count = 0).