Uma conjectura sobre finitude direta, incluída entre os problemas abordados pelos exemplos de grupos.
A OpenAI publicou no GitHub uma coleção de 722 estudos matemáticos produzidos por um modelo interno não disponível ao público, incluindo resultados distribuídos por 372 famílias de problemas. A empresa afirma que os trabalhos passam por diferentes etapas de verificação e que apenas parte deles foi verificada usando Lean.