Das Fellowship unterstützt Hausel und sein Team bei Project Sandbox. Vorgesehen sind Rechenleistung und Softwarezugang im Wert von 50.000 Euro über zwölf Monate. Project Numina ist eine gemeinnützige Organisation mit Sitz in Paris, die quelloffene KI für die Mathematik fördert. Das Vorhaben soll eine eigenständige Forschungsumgebung schaffen, in der Menschen und KI-Agenten mathematische Fragen untersuchen, Berechnungen ausführen und Beweise entwickeln.
Ausgangspunkt ist eine Familie offener Vermutungen. Das Team will darauf aufbauend eine neue Theorie entwickeln und prüfen, ob sich damit Beweise führen lassen. Ein menschlicher Mathematiker gibt dabei die Forschungsrichtung vor und beurteilt die Bedeutung der Ergebnisse. Die Agenten sollen unter anderem Werkzeuge erstellen, Vermutungen formulieren, Beweisversuche unternehmen und die Arbeit anderer Agenten überprüfen. Die Zusammenarbeit konzentriert sich auf Bereiche, die bislang nicht mit einem Beweisassistenten formalisiert wurden.
Project Sandbox soll Aussagen nicht ungeprüft in seine Dokumentation übernehmen. Rechnerische Behauptungen werden durch ein Computer-Algebra-Orakel kontrolliert; für formale Beweise ist ein Beweiskern vorgesehen. Dieser prüft, ob ein Beweis innerhalb eines festgelegten formalen Systems gültig ist. Er bewertet laut ISTA weder die Bedeutung noch die Eleganz eines Arguments. Als Inspiration und technischen Ausgangspunkt nennt Hausel den Numina-Lean-Agent, einen interaktiven mathematischen Beweisassistenten, der Anfang des Jahres vorgestellt wurde.
Inhaltlich soll das Projekt eine Verbindung zwischen Darstellungstheorie und äquivarianten Topologie untersuchen. Zu den genannten Themen gehören Quantengruppen und die Langlands-Klassifikation sowie affine Schubert-Varietäten und GKM-Graphen. Für die Visualisierung hat das Team bereits ein interaktives Werkzeug namens Eyepiece entwickelt. Hausel zufolge ist geplant, es für virtuelle Realität anzupassen und Funktionen hinzuzufügen, mit denen Nutzer:innen direkt mit den Berechnungen der Sandbox interagieren können.
