#lean

26 октября 2026 г.October 26, 2026 день целиком 1 новостьstory

AI Важно OpenAI опубликовала заявленное опровержение гипотезы экспоненциального времени, полученное внутренней модельюOpenAI publishes a claimed disproof of the Exponential Time Hypothesis produced by an internal model В репозитории openai/math появилась статья «The Exponential Time Hypothesis is False» с формализацией на Lean: алгоритм точного подсчёта решений k-CNF за субэкспоненциальное время. Если доказательство устоит — это переворот в теории сложности; проверку ведёт группа во главе с Импальяццо, Патури и Уильямсом.The openai/math repo added a paper titled "The Exponential Time Hypothesis is False" with Lean formalisations: an algorithm that exactly counts k-CNF solutions in subexponential time. If it holds, it upends complexity theory; a group led by Impagliazzo, Paturi and Williams is reviewing it.