A OpenAI publicou no GitHub setecentos e vinte e dois documentos matemáticos desenvolvidos pelo modelo interno de inteligência artificial. Estes manuscritos estão agrupados em trezentos e setenta e dois conjuntos de resultados e abrangem dezessete diferentes áreas da matemática.
Algumas das provas apresentadas foram formalizadas usando a linguagem Lean. Entre as conquistas do modelo está a obtenção de uma nova prova para o problema de Hadwiger-Nelson, que é um problema conhecido na área de geometria combinatória.
O modelo demonstrou que não é possível colorir um plano com cinco cores de tal forma que quaisquer dois pontos separados por exatamente uma unidade de distância tenham cores diferentes. Consequentemente, o número cromático do plano pode ser seis ou sete. Esta prova também foi formalizada no sistema Lean.