OpenAI выложила 719 математических рукописей, созданных ИИ

OpenAI опубликовала на GitHub 719 рукописей, сгенерированных внутренней фронтир-моделью, в 372 семействах результатов по 17 областям математики. Среди заявлений — доказательство гипотезы уникальных игр Хота 2002 года; около 42% ключевых результатов имеют формализацию в Lean.

• 719 рукописей в 372 семействах результатов по 17 областям математики
• Модель получила около 4000 задач, на результат уходило ~3 часа вычислений ChatGPT Pro
• Около 42% ключевых результатов формализованы в Lean
• Материалы выложены под лицензией Apache 2.0, сама модель не раскрыта