Как сообщает The Decoder, OpenAI привлекла внешних экспертов в роли «пастырей» результатов: ИИ-модели компании подготовили доказательства в трёх областях, и каждую проверяют по своей схеме. Часть доказательств переведена на язык Lean — это язык программирования, в котором компьютер автоматически проверяет каждый шаг доказательства. При этом Lean подтверждает лишь корректность рассуждения для записанного утверждения, а соответствует ли оно исходной задаче, решают люди.
В информатике, по словам компании, её система доказала ложность экспоненциальной временной гипотезы (ETH) о задаче выполнимости булевых формул (SAT) — можно ли присвоить переменным формулы значения «истина» и «ложь» так, чтобы она стала истинной. ETH утверждает, что в худшем случае время решения растёт экспоненциально; на этой гипотезе построены сотни работ по теории графов, вычислительной биологии, базам данных и вычислительной геометрии, и если доказательство устоит, они лишатся доказательной базы. Проверку ведут профессор MIT Райан Уильямс и авторы гипотезы Расселл Импаглаццо и Рамамохан Патури из Калифорнийского университета в Сан-Диего — без оплаты и без соглашений о неразглашении; OpenAI по их просьбе опубликовала все исходные данные, включая Lean-версию, и обещала профинансировать конференцию по итогам.
Математический результат касается гипотезы локального сглаживания о поведении волн — она описывает, что резкая концентрация волны в одной точке, как свет в фокусе линзы, кратковременна, а в среднем волны распределены ровнее. Гипотезу предложил Кристофер Согге в 1991 году, до этого её доказали только для двух измерений; по данным OpenAI, теперь есть доказательство для всех размерностей, из которого автоматически следуют гипотеза Какеи из геометрии (для трёх измерений её доказали лишь в 2025 году) и гипотеза ограничения Стайна из анализа Фурье. Для этого доказательства отдельной группы нет — по совету внешнего эксперта OpenAI сразу опубликовала текст и Lean-версию.
В физике, по заявлению компании, ИИ доказал, что ряд квантовых теорий поля — теория Янга — Миллса, квантовая хромодинамика и простейшая теория великого объединения — математически существует в четырёх измерениях; для теорий с взаимодействующими частицами такого результата раньше не было. Теория Янга — Миллса связана с одной из «задач тысячелетия» с премией $1 млн от Математического института Клэя, однако решена только часть о существовании, а не о «массовой щели» — минимальной ненулевой массе частиц, так что задача тысячелетия полностью не закрыта. Проверку ведёт группа нобелевского лауреата 2004 года Дэвида Гросса, куда входят Майкл Дуглас, Артур Джаффе, Игорь Клебанов и Никита Некрасов; она пока не публикует материалы ИИ и планирует сама подготовить изложение результата.
OpenAI подчёркивает, что не претендует на научный приоритет и отдаёт его группам, разъясняющим результаты. Компания также пообещала выделить $5 млн фонду Simons Foundation на семинары и конференции, посвящённые проверке ИИ-результатов; The Decoder связывает эти шаги с критикой OpenAI после истории с уравнениями Навье — Стокса.
Практическая отдача неочевидна: SAT-солверы, которые проверяют схемы микросхем и тестируют ПО, обычно работают с задачами, далёкими от худшего случая, описываемого ETH. Райан Уильямс в X допустил заметный прогресс практического решения SAT в течение 12 месяцев, но уточнил: «Или мы можем не увидеть ничего подобного. Я действительно не знаю».
