Задачи OpenAI для Comparator решаются подменой определения

Есть задача: доказать, что плоскость нельзя раскрасить в пять цветов так, чтобы любые две точки на расстоянии 1 получили разные цвета. Автор блога Ohaithe формально «доказал» это, просто объявив само понятие правильной раскраски ложным. Comparator принял такую подмену в задаче-челлендже из математического релиза OpenAI, и, по словам автора, ещё шесть задач сломаны так же.

Коротко

• В JSON-файлах нескольких задач для Comparator определения, которые должны быть зафиксированы, перечислены в поле definition_names, а всё из этого поля участник может свободно переписать.
• В EuclideanFiveColor.lean автор заменил ProperColoring на False, после чего теорема no_proper_five_coloring доказывается выражением в одну строку, и Comparator засчитывает такое решение.
• Ещё шесть задач сломаны так же, среди них Bernier, LogspaceEquality, KServer и Naimark, а закономерности в том, какие определения попали в уязвимое поле, автор не находит.

Если вы не следили: по данным Developers Digest, 1 августа 2026 года OpenAI опубликовала десять результатов по математике и теоретической информатике. Каждый из них решает задачу, где главный вопрос не сдвигался минимум десять лет, и к каждому приложен сертификат на Lean 4. Там же пишут, что результаты получила внутренняя версия Astra, а потраченные токены стоили бы около 2 000 долларов по тарифам Sol API. В репозитории openai/ten-proofs на GitHub для независимой проверки через Comparator дана ссылка на README каталога ComparatorChallenges.

В EuclideanFiveColor.lean всё решение свелось к замене определения на False

Файл EuclideanFiveColor.lean почти пустой. В нём одно определение, ProperColoring: раскраска комплексной плоскости в colorCount цветов считается правильной, если любые две точки на расстоянии ровно 1 окрашены по-разному. Рядом одна теорема, no_proper_five_coloring: правильной раскраски в пять цветов не существует. На месте доказательства стоит sorry, заглушка, которую участник должен заменить настоящим выводом.

В сопроводительном JSON теорема OAI.EuclideanFiveColor.no_proper_five_coloring указана в поле theorem_names, а определение OAI.EuclideanFiveColor.ProperColoring указано в поле definition_names. Автор проверил на практике, что Comparator примет решение, в котором определение раскраски переписано вот так:

def ProperColoring (colorCount : ℕ) (coloring : ℂ → Fin colorCount) : Prop := False

Если правильной раскраски не бывает по определению, теорема доказывается сама собой: доказательство занимает одну строку, fun ⟨_, h⟩ => h. Автор оговаривается, что в этом случае подмену легко заметить, ведь определение стоит в самом начале файла, который импортирует только Mathlib.

Bernier, LogspaceEquality, KServer и Naimark закрываются тривиальным доказательством

По словам автора, ещё в шести задачах файл для Comparator устроен так же, и их тоже можно закрыть тривиальным доказательством. Среди них Bernier, KServer, Naimark и LogspaceEquality. Последняя формализует утверждение L=RL=BPL: вероятностные вычисления с логарифмической памятью не мощнее детерминированных.

Отдельно автор разбирает OccupiedOverlapRokhlinSpinAngle. Там в одном определении стоит законный sorry, но он означает обязательство что-то доказать, пустого места для ответа там нет. При этом Comparator разрешает менять всё остальное определение. Кроме того, в том же списке есть ещё два определения вовсе без sorry.

Не всякое определение в definition_names ошибочно. В ElementaryPositivity тоже есть определение, которое заполняет участник, и автор считает это корректным: главная цель задачи там объект, несущий данные, а не утверждение. Закономерности в том, что получило такую обработку, автор не видит. Часто из большого файла в поле попадают лишь несколько определений. По его сведениям, до его поста об этом нигде не писали.

Comparator доверяет списку definition_names, а смысл задачи не сверяет

Вот как устроена проверка. В JSON задачи два списка. В theorem_names перечислены утверждения, которые участник обязан доказать в исходной формулировке. В definition_names перечислены определения, которые участник вправе задать сам, и их содержимое на решение Comparator не влияет.

Представьте экзаменационный бланк, где серые поля заполняет экзаменатор, а белые студент. Если по ошибке оставить белым поле с условием задачи, студент впишет туда удобное условие, и бланк формально будет заполнен верно. Белые поля нужны там, где ответом служит сам объект, как в ElementaryPositivity. Для утверждения вроде «правильной раскраски нет» такое поле делает задачу пустой.

Сами доказательства в ten-proofs собраны на Lean 4.32.0 с библиотекой mathlib и системой сборки Lake. Developers Digest, описывая релиз, писал, что человек проверяет 40-страничное доказательство месяцами и всё равно может пропустить тонкий пробел. Сертификат Lean, по той же статье, либо компилируется, либо нет.

Стоит оговорить, чего находка не утверждает. Автор не пишет, что сами доказательства OpenAI неверны. Он показывает другое: независимая проверка через Comparator в этих задачах не ловит подмену условия, причём вручную он подтвердил её на одном примере. На наш взгляд, в этом и состоит слабое место довода про сертификаты: компилятор Lean проверяет вывод, но не сверяет формулировку с исходной, так что один список в JSON весит не меньше самого доказательства.

Что будет с октябрьскими 162 формализациями

Как и когда OpenAI поправит файлы задач, пока не сообщается. Открытым остаётся и вопрос о следующем релизе. По данным Metirai, 6 октября 2026 года OpenAI выложила в репозиторий openai/math 722 рукописи в 372 семействах, и Lean-формализация есть у главного результата 162 из них. Проверяли ли их файлы на ту же ошибку, пока неизвестно.