Die Liste reicht von einer behaupteten Verbesserung des allgemeinen Kugelpackungs-Exponenten seit 1978 über eine explizite nicht-sofische Gruppe bis zu Gegenbeispielen für Vermutungen von Connes sowie Erdős und Simonovits. OpenAI bezeichnet die Resultate als eigene Fortschritte; ein unabhängiges mathematisches Gutachten liegt noch nicht vor.
Die Lean-Dateien sollen zeigen, dass die formalisierten Aussagen aus den Axiomen von mathlib folgen. Sie prüfen damit den formalisierten Beweis, aber nicht automatisch, ob Definitionen und Aussage genau der klassischen Vermutung entsprechen. Das Repository enthält die zehn Formalisierungen unter Apache 2.0.