Una conjetura sobre la finitud directa, incluida entre los problemas abordados por los ejemplos de grupos.
OpenAI publicó en GitHub una colección de 722 estudios matemáticos producidos por un modelo interno no disponible para el público, que incluye resultados distribuidos en 372 familias de problemas. La empresa confirma que los trabajos atraviesan distintas etapas de verificación y que solo una parte de ellos ha sido verificada mediante Lean.