Anthropic опубликовала машинно проверенное доказательство одной из самых известных нерешённых гипотез теории вероятностей. Модель искусственного интеллекта показала, что в классической задаче о перколяции фазовый переход остаётся непрерывным во всех размерностях, закрыв пробел для пространств от трёх до десяти измерений. Само доказательство уже проверяется системой формальной математики, однако независимое рецензирование специалистами ещё не завершено.
Теория перколяции изучает, как множество случайных связей вдруг превращается в единую протяжённую сеть. Представить модель проще всего как бесконечную решётку из труб: каждая труба независимо открыта с вероятностью p. Пока открытых участков мало, вода сможет пройти лишь через небольшие области. После некоторого критического значения pc появляется вероятность построить путь, который уходит сколь угодно далеко.
Главная загадка касалась самого момента перехода. Математики хотели понять, существует ли бесконечная связная область уже точно при p = pc, либо возникает только после пересечения критической точки. На языке теории вероятностей вопрос записывают как θ(pc) = 0. Нулевое значение означает, что в самой критической точке бесконечного кластера ещё нет, а переход происходит непрерывно.
Новая работа не вычисляет значение pc. Такая формулировка была бы неверной: точные критические вероятности для большинства многомерных решёток по-прежнему неизвестны. Модель Anthropic доказала другое, но не менее важное утверждение, касающееся поведения системы непосредственно на границе фазового перехода. Для двумерного случая результат был известен давно, а методы для пространств высокой размерности позволяли закрыть случай с 11 измерениями и выше. Неохваченными оставались размерности от трёх до десяти, и именно этот разрыв теперь закрывает новое доказательство.
ИИ не пытался напрямую разобрать бесконечную решётку во всей её сложности. Ключом стало опубликованное в 2024 году сведение задачи к другому утверждению. Гади Козма и Шахаф Ницан показали, что знаменитая гипотеза последует из определённого неравенства для вероятностей соединения частей случайного графа. Само неравенство тогда оставалось гипотезой.
Модель Anthropic пошла дальше и доказала более сильное неравенство, из которого нужное утверждение Козмы и Ницана получается как следствие. Затем формальная цепочка приводит к θ(pc) = 0 для перколяции по рёбрам между ближайшими соседями в решётке Zd при любой размерности d ≥ 2. Опубликованное доказательство заново выводит и ряд классических результатов, которые нужны для всей цепочки, вместо того чтобы просто принимать их без проверки.
Особенность работы в том, что математические рассуждения записаны не только обычным текстом. Авторы формализовали их на языке Lean, где компьютер проверяет каждый логический переход. Такой подход резко отличается от ситуации, когда языковая модель выдаёт убедительно звучащие формулы, а человеку приходится самостоятельно искать скрытую ошибку среди десятков страниц рассуждений.
Формальная проверка всё же не ставит окончательную точку. Lean подтверждает, что вывод действительно следует из записанных определений и допущений и что внутри формального доказательства нет пропущенных логических шагов. Но компьютер не решает другой важный вопрос: совпадает ли формализованное утверждение во всех деталях с той математической гипотезой, которую собирались доказать. В материалах проекта прямо указано, что независимое рецензирование ещё не проводилось, поэтому специалистам предстоит проверить саму постановку и математический смысл формализации.
Ещё недавно модели в основном проверяли на олимпиадных задачах и уже известных теоремах, а теперь системы находят контрпримеры и строят доказательства для проблем, которыми профессиональные математики занимались десятилетиями. При этом правильное доказательство не всегда автоматически означает полноценное научное открытие: нужно проверить новизну результата, соответствие исходной задаче, использованные идеи и возможные связи с прежними работами.
Если независимая проверка подтвердит формализацию, математики наконец получат общий ответ для классической решётки любой размерности: в критической точке бесконечного связного кластера не возникает. Не менее важным окажется способ, которым найден ответ. ИИ здесь выступил не как калькулятор или поисковик, а как система, построившая новый математический аргумент и доведшая его до формы, которую может построчно проверить другой компьютер.
