Новая внутренняя модель логического вывода OpenAI разом представила десять поразительных математических достижений.
Среди них:
- Впервые доказано существование несофических групп (Non-sofic groups);
- Представлены новые нижние границы для схем (Circuit lower bounds);
- Покорён предел сложности задачи о ближайшем векторе (Closest Vector Problem, CVP);
- А также теорема об экспоненциальном затухании при параллельном повторении квантовых игр для двух игроков (Quantum parallel repetition).
Больше всего доцента Колумбийского университета Генри Юэна волнует последнее —
В 2016 году Юэн добился значительного прогресса в этой проблеме, но полностью не решил её. За 10 лет он терпел неудачу за неудачей, и даже месяц назад он снова штурмовал окончательное доказательство с помощью ChatGPT 5.5, но почти безрезультатно.
А ИИ, стоя на его плечах, легонько пнул мяч и отправил его в ворота.
Доказательство верное, но человек его не понимает
Несколько дней назад Лицзе Чэнь отправил Генри Юэну и ещё нескольким людям черновик статьи.
В тот момент жизнь была слишком занятой, и у него не было времени глубоко её изучить. Теперь статья опубликована. Ему не терпится высказаться.
Теорема о квантовом параллельном повторении (Quantum parallel repetition theorem) — это область, которой Генри Юэн посвятил годы усердной работы в аспирантуре и которой он больше всего гордится.
Генри Юэн, доцент кафедры компьютерных наук семьи Ср��вани в Колумбийском университете
Он помнит те послеобеденные часы, проведённые в кафе, глубокие ночи в офисе и бесчисленные выходные, которые должны были быть отдыхом, но он снова и снова разбирал и изучал классическую теорему о параллельном повторении Рана Раза.
Он хотел решить квантовую версию этой теоремы, не мог из-за этого спать по ночам, ворочаясь с боку на бок. Он проглотил тонны математических инструментов и в итоге успешно доказал полиномиальное затухание.
https://arxiv.org/pdf/1604.04340
Что ещё важнее, он обрёл уверенность в себе, наконец осознал свои способности и доказал, что действительно может решать (по крайней мере, некоторые) проблемы, которые волнуют и других.
Он уверен, что это доказательство от OpenAI, вероятно, верное, ведь уже есть формализованное доказательство в Lean. Но чтобы переварить это новое доказательство, Генри Юэну потребуется некоторое время.
Хотя новое доказательство действительно продолжается с того места, где он остановился, ИИ преодолел ограничения его первоначальной стратегии доказательства, используя некоторые приёмы и методы. Возможно, эти методы уже известны исследователям в области теории операторов (operator theory) и функционального анализа (functional analysis).
Помимо волнения, первым чувством Юэна было разочарование — разочарование стилем написания статьи.
По его словам, это доказательство читается так, словно оно написано ИИ: долгие преамбулы, которые долго ходят вокруг да около, а ключевые моменты появляются словно по волшебству, сбивая с толку.
Доказательство OpenAI читать интересно, но и немного головоломно.
Оно сначала аккуратно ставит проблему на стол, а затем внезапно прыгает в направлении «использовать резольвенту для поиска правильного очищения (purification)», почти не оставляя логических ступеней между ними.
Далее следует серия довольно нетривиальных вычислений матричной энтропии, которые извилисто продолжаются, и в конце вам говорят: этот путь работает.
Но о том, откуда взялась эта ключевая интуиция, оно умалчивает.
А самый изящный, самый творческий момент — использование трюка с раздутием пространства операторов с помощью преобразования Ульмана (Uhlmann transformation), который должен был стать самым захватывающим кульминационным моментом всего доказательства, — был выброшен ИИ как ненужный мусор, безо всякого предупреждения и объяснения, в четвёртом разделе.
Правильное доказательство, скрывающее самую важную идею.
Он надеется, что OpenAI потратит ещё несколько подсказок, чтобы как следует структурировать этот текст.
Что ранит ещё сильнее — второй слой: Проверка Lean'ом не равносильна пониманию.
Машина может гарантировать, что каждый шаг вывода безупречен, но вопросы «почему этот трюк работает», «что он означает в более широкой теоретической картине», «где ещё его можно применить» — на них Lean не может ответить.
Юэн признаётся, что до сих пор переваривает это доказательство.
Ответ лежит перед ним, но ему приходится, как при чтении статьи дилетанта, строчка за строчкой восстанавливать интуицию, о которой ИИ умолчал.
Да, там есть доказательство на Lean. Но это лишь формализация, не означающая, что я его понял. Чтобы по-настоящему переварить, видимо, придётся медленно работать над ним.
Действительно, ИИ расширил границы человеческого понимания, но что дальше? Какая радость и смысл остаются в исследованиях? Если ИИ решит все задачи, которые его мучили, что ему останется?
Вопросы следуют один за другим. Но одну вещь он осознаёт всё яснее: у математиков впереди не будет времени скучать — им придётся и укрощать этих интеллектуальных гигантов, и переводить их жаргон на понятный человеческий язык.
«Опровержение» ИИ столетней математической гипотезы оказалось фейком! И Lean — не сейф
На прошлой неделе Рамана Кумар с помощью 300 строк кода на Lean «опроверг» самую известную нерешённую математическую гипотезу — «гипотезу Коллатца» (Collatz conjecture).
Её вопрос очень прост: взяв натуральное число, следуйте двум правилам — если число чётное, разделите его на 2; если нечётное, умножьте на 3 и прибавьте 1 — независимо от того, с какого числа вы начали, попадёте ли вы в итоге к 1?
Можете сами проверить:
Гипотеза утверждает, что какое бы натуральное число вы ни взяли, вы в итоге попадёте в этот цикл 4→2→1.
С момента, когда математик Лотар Коллатц сформулировал её в 1937 году, никто не смог ни доказать её истинность, ни найти контрпример.
Математик Пол Эрдёш назвал её: «Математика ещё не готова к таким проблемам», а член Национальной академии наук США, математик Джеффри Лагариас считает, что «это исключительно трудная проблема, полностью находящаяся за пределами возможностей современной математики».
Если бы она была опровергнута, это стало бы сенсацией в математическом мире.
К сожалению, через 3 дня это формализованное доказательство на Lean было признано недействительным, поскольку фактически оно лишь использовало уязвимость на низком уровне в ядре Lean.
Даниэль Сельсам из OpenAI вместе с ИИ, специализирующимся на кибербезопасности, помогли Lean FRO провести аудит ядра.
В итоге они обнаружили в ядре Lean не одну уязвимость!
Почти одновременно профессор математики Университета Рутгерса, консультант специализированной исследовательской группы по Lean Алекс Конторович опубликовал пост с предупреждением: не считайте Lean всемогущим верификатором.
Он указал на ахиллесову пяту — семантическое соответствие (Semantic Alignment).
Даже если ядро Lean безупречно, Lean проверяет только компиляцию кода. Кто гарантирует, что ваше «определение», записанное в коде, соответствует «интуитивному замыслу», который люди вкладывают в естественный язык?
Lean может подтвердить только одно: код компилируется, формальная логика безупречна. Но он абсолютно не проверяет более важный вопрос: Соответствует ли это формальное утверждение той теореме, которую вы хотели доказать?
Теорема доказана правильно, но условие переписано неверно — Lean всё равно даст зелёный свет.
А эта проблема соответствия не может быть решена чисто компьютерными методами.
В своём выступлении на ICM 2026 Конторович уже отмечал: самое большое слепое пятно формальной математики не в том, чтобы «сделать правильный вывод», а в том, чтобы «правильно сформулировать». Последнее слово должно оставаться за экспертами-людьми.
Почему эксперимент Liquid Tensor Experiment стал легендарным? Именно благодаря почти одержимому ручному контролю исследователей за каждым математическим определением.
Слова обоих профессоров указывают на один и тот же факт: ИИ может доказывать, машина может проверять, но понимание и контроль — всё ещё дело человека.
В конце ещё одна сплетня о модели логического вывода от ИИ:
Источники:
https://www.henryyuen.net/posts/on-openai-and-quantum-parallel-repetition/
https://x.com/AlexKontorovich/status/2083919186825236831
https://x.com/henryquantum/status/2083623700608237956
Статья из WeChat Official Account «Новая Эра ИИ» («新智元»), автор: ASI Revelation; редактор: Давид
