OpenAI переложила узкое место математики с поиска доказательств на их проверку
Внутренняя модель получила около 4000 открытых задач и подготовила 722 рукописи, объединенные в 372 семейства результатов.
Для 162 работ опубликованы формализации в Lean, но весь каталог еще не прошел независимую проверку.
Средний результат потребовал вычислений, сопоставимых с тремя часами работы ChatGPT Pro в режиме рассуждений.
Почему важно
Если заметная доля доказательств выдержит проверку, дефицитом в математике станут постановка задач, независимая экспертиза и понимание результатов.