Une conjecture sur la finitude directe, mentionnée parmi les problèmes abordés par les exemples de groupes.
OpenAI a publié sur GitHub une collection de 722 études mathématiques produites par un modèle interne non accessible au public, comprenant des résultats répartis sur 372 familles de problèmes. L’entreprise précise que les travaux se trouvent à différents stades de vérification et qu’une partie seulement a été vérifiée à l’aide de Lean.