OpenAI выложила 722 математических доказательства, 42% проверены формально

6 октября 2026 года OpenAI опубликовала на GitHub репозиторий openai/math с 722 рукописями, сгруппированными в 372 семейства результатов, на каждое ушло в среднем три часа вычислений ChatGPT Pro. На следующий день три рукописи отозвали из-за ошибки в знаке, а заявленные 42% формализации в Lean оспариваются: независимые подсчёты дают 24% или 36%.

• Репозиторий openai/math: 722 рукописи в 372 семействах результатов
• 7 октября отозваны три рукописи из-за ошибки в знаке, осталось 719
• Заявлено 42% формализации в Lean, независимые подсчёты — 24% и 36%
• Модель, написавшая доказательства, публично недоступна