OpenAI опубликовала 722 математические рукописи, созданные внутренней ИИ-моделью 😮 В подборке — теоремы, доказательства и результаты по открытым исследовательским задачам. Рукописи объединены в 372 группы связанных результатов: среди них есть основные работы, следствия и альтернативные доказательства. Многие доказательства формализованы в Lean — языке, который позволяет компьютеру проверять математические доказательства. Проверка всей подборки ещё не завершена. OpenAI прямо предупреждает: результаты находятся на разных стадиях проверки, а работы без формализации могут содержать ошибки. Эти результаты получила ещё не выпущенная модель OpenAI, название которой компания пока не раскрывает. OpenAI работает над её выпуском, но сроки не объявлены. Подробнее #исследования #апдейтымоделей