Eine Vermutung zur direkten Endlichkeit, die zu den Problemen gehörte, die in den Beispielen von Gruppen behandelt wurden.
OpenAI hat auf GitHub eine Sammlung mit 722 mathematischen Studien veröffentlicht, die von einem internen, nicht öffentlich verfügbaren Modell erzeugt wurden und Ergebnisse aus 372 Problemfamilien umfasst. Das Unternehmen betont, dass sich die Arbeiten in unterschiedlichen Prüfphasen befinden und nur ein Teil von ihnen mit Lean verifiziert wurde.