Компания OpenAI опубликовала на GitHub коллекцию из 372 математических доказательств, сгенерированных внутренней передовой моделью. Многие из них сопровождаются формализацией на языке Lean для машинной проверки. По заявлению компании, каждое решение в среднем потребовало около трех часов вычислительных мощностей уровня ChatGPT Pro. В коллекцию вошли результаты, касающиеся компьютерных алгоритмов и гипотезы Римана. OpenAI также утверждает, что та же модель ранее нашла решение задачи Навье-Стокса, которое сейчас проходит формальную проверку. Публикация на GitHub вместо академических журналов призвана ускорить процесс ознакомления с результатами, объем которых может превысить возможности ручного рецензирования. Однако 25 лауреатов Филдсовской премии выразили обеспокоенность в открытом письме, предупредив, что массовое производство математических истин может обесценить концептуальное понимание и глубину науки. Математики опасаются, что в будущем литература станет настолько обширной, что человеческое сообщество перестанет ее понимать.