Суть прорыва: гипотеза, которая ждала 50 лет
10 октября OpenAI заявила, что модель GPT-5.6 Sol Ultra нашла доказательство гипотезы о двойном покрытии циклов (Cycle Double Cover Conjecture). Эта задача теории графов, сформулированная независимо Джорджем Секерешем (1973) и Полом Сеймуром (1979), утверждает, что в любом графе без мостов существует набор циклов, покрывающих каждое ребро ровно дважды. Несмотря на простоту формулировки, общий случай оставался открытым пятьдесят лет, упираясь в сложный класс графов — снарки.
Техническая реализация: 64 сабагента и жесткий промпт
Решение было найдено менее чем за час с использованием архитектуры из 64 параллельных сабагентов. Процесс включал:
- Ролевое разделение: Sol Ultra генерировала логику, Codex и GPT-5.6 Sol оформляли текст.
- Анти-отступление: Промпт запрещал модели искать готовые решения, ссылаться на открытые задачи или признавать сложность. Требовалось действовать «как будто доказательство уже существует».
- Adversarial-проверка: Специальные агенты искали лазейки, краевые случаи и логические ошибки в каждом кандидате на доказательство.
Структура доказательства
Доказательство занимает всего три страницы и опирается на классические инструменты середины XX века, а не на новые теории. Ключевые элементы:
| Этап | Метод/Теорема | Значение |
|---|---|---|
| Сведение | К кубическим графам (Франсуа Джагер) | Упрощение структуры графа до вершин степени 3 |
| Разметка | Теорема о 8-потоке (Килпатрик и Джагер, 1970-е) | Согласованная разметка ребер графов без мостов |
| Ключевой ход | Векторное пространство и линейная алгебра | Превращение разметки в пары элементов для покрытия циклами |
Статус верификации и контекст
На данный момент доказательство не прошло формальной верификации в системах типа Lean и не рецензировано. Википедия уже добавила в статью о гипотезе формулировку, что OpenAI «заявила» о решении, подчеркивая статус утверждения. Это не первый случай успеха OpenAI в математике: в мае модель помогла опровергнуть ожидавшийся ответ в задаче Эрдеша №90, что было подтверждено ведущими математиками (Томас Блум, Уилл Савин, Тимоти Гауэрс).
Если доказательство выдержит проверку сообщества, это станет первым случаем полного закрытия именованной гипотезы с полувековой историей силами ИИ. Если нет — гипотеза пополнит список несостоявшихся машинных попыток.
Источник: Habr ↗