群の例で扱われた問題の一つとして挙げられた、直有限性に関する予想。
OpenAIは、一般公開されていない社内モデルが生成した数学研究722件を収録するコレクションをGitHubで公開した。結果は372の問題族に分散しており、同社は研究がさまざまな検証段階にあること、一部のみがLeanを使って検証済みであることを強調している。