OpenAI выложила математику от внутренней модели: Lean и GitHub

OpenAI выложила широкий набор математических результатов внутренней передовой модели в GitHub-репозиторий — с протоколами пересмотра статей и правилами цитирования. Формат выбирали вместе с независимой Advisory Group on Mathematics and Artificial Intelligence при Institute for Advanced Study; на публичные рекомендации группы опирались при публикации.

Что лежит в репозитории

• формализации многих доказательств в Lean — список обещают дополнять по мере готовности;
• 10 сводок рассуждений модели;
• оценка вычислительных затрат в пересчёте на использование ChatGPT Pro;
• статистика по числу попыток решить задачи.

В среднем на типичный результат ушёл эквивалент примерно трёх часов думающего режима Pro. OpenAI также финансирует воркшопы, конференции и спецпрограммы по разбору крупных математических результатов от ИИ и готовит ответственный релиз модели, которая получила эти теоремы.

Источник: Sharing AI progress in mathematics.