вторник, 30 июня 2026 г.

Claude доказал гипотезу, которую люди не могли закрыть с 2014 года

22 июня 2026 года исследователи из Гарварда и MIT опубликовали на arXiv статью «A Machine-Verified Proof of a Quantum-Optimization Conjecture». В ней они сообщают о machine-verified решении гипотезы Farhi, Goldstone и Gutmann (FGG), открытой с 2014 года.

Доказательство найдено с помощью Claude Fable 5. Верификация выполнена end-to-end в Lean 4.

Что за гипотеза

FGG Conjecture (2014): Гипотеза о Quantum Approximate Optimization Algorithm (QAOA) на графе «ring of disagrees».

Утверждение: QAOA глубины p достигает approximation ratio ровно (2p+1)/(2p+2).

Почему важно: QAOA — один из главных алгоритмов для near-term квантовых компьютеров. Точное понимание его approximation ratio критично для оценки квантового преимущества.

Почему открыта с 2014: Доказательство требовало анализа сложной тригонометрической структуры с nested зависимостями. Стандартные подходы не работали.

Как решили

Команда:

Uri Kol, Center of Mathematical Sciences and Applications, Harvard

Maor Ben-Shahar, MIT Center for Theoretical Physics

Kfir Sulimany, Research Laboratory of Electronics, MIT

Dirk Englund, Research Laboratory of Electronics, MIT

Метод:

Исследователи свели задачу к одному недоказанному утверждению

Отформализовали задачу в custom Lean infrastructure

Отдали Claude Fable 5

Claude нашел скрытую симметрию, которую не видели люди

Claude сгенерировал аргумент

Lean 4 независимо верифицировал доказательство

Ключевая находка Claude: Скрытая симметрия в структуре задачи. Модель обнаружила паттерн, который упрощал доказательство до формы, поддающейся верификации.

Почему это важно

Не «ИИ что-то выдал»: Это сертифицированное доказательство. Lean 4 — формальный proof assistant, который проверяет каждый шаг логики. Если Lean принял доказательство, оно математически корректно.

Первое в квантовой оптимизации: Это первое machine-verified решение открытой проблемы в области quantum optimization.

Human-AI collaboration: Люди сформулировали задачу, построили формальную инфраструктуру, направляли процесс. Claude нашел ключевой insight. Lean верифицировал результат.

Контекст: волна AI-доказательств

Donald Knuth + Claude Opus 4.6 (март 2026): Knuth опубликовал «Claude's Cycles» — статью, где благодарит Claude за решение открытой задачи по теории графов, над которой он работал десятилетия. Claude нашел конструкцию за ~1 час в 31 guided exploration. Kim Morrison из Lean community формализовал доказательство Knuth за несколько дней.

Knuth (исторически скептичный к LLM):

«It seems I'll have to revise my opinions about 'generative AI'. What a joy it is to learn not only that my conjecture has a nice solution but also to celebrate this dramatic advance in automatic deduction and creative problem solving.»

Terence Tao + GPT-5.2: Tao принял proof для Erdős Problem #397, верифицированный в Lean.

DeepMind: AI-assisted система решила 9 задач Erdős через Lean.

С конца 2025: Более дюжины ранее открытых математических проблем переведены в статус «solved» с AI-моделями в credits.

Различие ролей

Что делает AI:

Находит паттерны и конструкции

Генерирует аргументы

Исследует solution space

Что делает человек:

Формулирует задачу

Строит формальную инфраструктуру

Направляет exploration

Пишет финальный proof (в некоторых случаях)

Что делает Lean:

Верифицирует каждый шаг логики

Гарантирует математическую корректность

Ловит ошибки, которые пропустили бы и AI, и человек

Как отмечает один исследователь: «Claude found a construction that works. The humans wrote the proof. Those are different things.»

Инструменты

Claude Fable 5:

Mythos-class модель Anthropic, released 9 июня 2026

Первая generally available модель этого класса

State-of-the-art на большинстве бенчмарков

Lean 4:

Interactive theorem prover

Dependently-typed programming language

Проверяет каждый шаг proof

Custom Lean infrastructure:

Исследователи построили специализированную инфраструктуру для autoformalization

Это позволило перевести задачу в форму, с которой мог работать Claude

Что дальше

Авторы описывают свой подход как комбинацию:

Human-guided autoformalization

Custom Lean infrastructure

Large language model capabilities

Этот pipeline может быть применен к другим открытым проблемам в квантовой информатике и за её пределами.

Итог

Исследователи из Гарварда и MIT использовали Claude Fable 5 для доказательства гипотезы FGG — открытой проблемы в квантовой оптимизации с 2014 года.

Claude нашел скрытую симметрию. Lean 4 верифицировал доказательство end-to-end. Это не галлюцинация и не «что-то похожее на правильный ответ». Это сертифицированное математическое доказательство.

Вместе с работами Knuth (Claude's Cycles) и Tao (Erdős Problem #397) это формирует паттерн: AI-модели начинают вносить реальный вклад в математические исследования, а formal verification systems гарантируют корректность.