OpenAI и Anthropic заявили об опровержении гипотезы ETH

Гипотеза ETH, сформулированная в 1999 году, утверждает, что задачу 3-SAT нельзя решить за субэкспоненциальное время по числу переменных. OpenAI сообщила, что её внутренняя модель разработала детерминированный алгоритм, решающий 3-SAT за субэкспоненциальное время, а также подсчитывающий количество удовлетворяющих комбинаций (#3-SAT). Доказательство получено 16 октября и 17 октября формализовано в Lean. Anthropic опубликовала работу A 2^o(n) Time Algorithm for 3-SAT, автором которой указан Claude; компания утверждает, что её модель независимо получила другой алгоритм с аналогичным результатом, также с формальным доказательством на Lean 4 и проверкой независимым ядром nanoda. Предложенные алгоритмы дают асимптотическое улучшение, то есть преимущество проявляется при чрезвычайно больших размерах задачи, и пока мало что меняют для практических вычислений. Опровержение ETH не решает проблему P против NP.