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