Claude независимо нашла субэкспоненциальный алгоритм для 3-SAT

🧪️️️️️️ На следующий день после того, как OpenAI объявила, что её модель опровергла гипотезу экспоненциального времени, Anthropic сообщила: внутренняя модель Claude независимо нашла другое опровержение в тот же самый день, что и модель OpenAI, - 16 октября. Anthropic опубликовала статью «A 2^o(n) Time Algorithm for 3-SAT» с автором «Claude, Anthropic». Детерминированный алгоритм решает 3-SAT за субэкспоненциальное время, что опровергает Exponential Time Hypothesis. Он же считает и число выполняющих наборов в задаче #3-SAT. Ядро алгоритма 16 октября нашла внутренняя исследовательская модель Claude: 14 миллионов выходных токенов и ни одной человеческой подсказки. Сегодня доказательство оформлено в Lean 4, 1050 модулей поверх Mathlib, проверка ядром Lean и независимым чекером nanoda. По словам Anthropic, Claude Opus 5.5 может вывести результат заново по короткому техническому наброску. OpenAI почти одновременно заявила о собственном опровержении ETH. Оговорки в самой статье. Формализацию писали ИИ-модели и проверяли другие экземпляры тех же моделей, и ни один человек пока не известен как проверивший её целиком. Результат чисто асимптотический: для типичной формулы выигрыш у перебора появляется лишь при числе переменных порядка 10^10000, к решению формул на практике и к вопросу P против NP он не приближает. В Challenge.lean остаются два sorry, это две теоремы без доказательств для проверки. https://github.com/anthropics/formal-math/tree/16a5ce41304fcdaea4e0be7c132e1c361dc26da5/eth @ai_machinelearning_big_data #Anthropic #Claude