В репозитории
openai/math — результаты работы пока не выпущенной внутренней модели над открытыми исследовательскими задачами. OpenAI расширила такие испытания после того, как результаты на прежних математических тестах достигли насыщения.Что опубликовано:
🔘719 рукописей в 372 группах связанных работ: основные результаты, сопутствующие аргументы, следствия и альтернативные доказательства.
🔘PDF, исходники и сокращённые описания рассуждений по отдельным задачам.
🔘По данным OpenAI, 300 основных результатов — около 42% — формализованы на Lean, системе машинной проверки математических доказательств.
Проверка уже приносит исправления. 7 октября три рукописи отозвали: ошибка знака сломала аргумент в одной работе и конструкцию, на которую опирались ещё две. В 14 других рукописях внесли исправления. Поэтому считать всю коллекцию списком окончательно решённых проблем преждевременно.
Для разработчиков AI-агентов здесь практический урок: генерацию стоит связывать с независимой проверкой и отслеживанием зависимостей. Одна ошибка способна испортить целую цепочку последующих выводов.
Пруфы:
⏩репо
⏩история исправлений
#ai #openai #math #lean #formalverification #agents
@data_engi
