Anthropic опубликовала машинно проверенное доказательство одной из известных нерешённых гипотез теории вероятностей. Модель показала, что в задаче о перколяции фазовый переход остаётся непрерывным во всех размерностях, закрыв пробел для пространств от трёх до десяти измерений. Доказательство уже проверяется системой формальной математики Lean, но независимое рецензирование специалистами ещё не завершено.

Теория перколяции изучает, как множество случайных связей превращается в единую протяжённую сеть. Представьте бесконечную решётку из труб: каждая открыта с вероятностью p. Пока открытых участков мало, вода проходит лишь через небольшие области. После критического значения pc возникает вероятность построить путь, уходящий сколь угодно далеко.

Математиков интересовал сам момент перехода. Существует ли бесконечная связная область уже при p = pc, либо возникает только после? На языке теории вероятностей это записывают как θ(pc) = 0. Нулевое значение означает, что в критической точке бесконечного кластера ещё нет, переход происходит непрерывно.

Новое доказательство не вычисляет pc — точные критические вероятности для большинства многомерных решёток неизвестны. Модель доказала другое: поведение системы непосредственно на границе фазового перехода. Для двумерного случая результат был известен давно, методы для 11 измерений и выше позволяли закрыть эти случаи. Пробел оставался в размерностях от трёх до десяти — именно его и закрывает новое доказательство.

ИИ не пытался разобрать бесконечную решётку во всей сложности. Ключом стало опубликованное в 2024 году сведение задачи к другому утверждению. Гади Козма и Шахаф Ницан показали, что знаменитая гипотеза последует из определённого неравенства для вероятностей соединения частей случайного графа. Само неравенство оставалось гипотезой.

Модель Anthropic доказала более сильное неравенство, из которого утверждение Козмы и Ницана получается как следствие. Формальная цепочка приводит к θ(pc) = 0 для перколяции по рёбрам между ближайшими соседями в решётке Zd при любой размерности d ≥ 2. Доказательство заново выводит и классические результаты, необходимые для всей цепочки.

Математические рассуждения записаны не только текстом. Авторы формализовали их на языке Lean, где компьютер проверяет каждый логический переход. Это отличается от ситуации, когда языковая модель выдаёт убедительные формулы, а человеку приходится искать скрытую ошибку среди десятков страниц.

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

Модели раньше проверяли на олимпиадных задачах и известных теоремах. Теперь системы находят контрпримеры и строят доказательства для проблем, которыми профессиональные математики занимались десятилетиями. Правильное доказательство не всегда означает полноценное научное открытие: нужна проверка новизны, соответствия задаче, используемых идей и связей с прежними работами.

Если независимая проверка подтвердит формализацию, математики получат общий ответ для классической решётки любой размерности: в критической точке бесконечного связного кластера не возникает. Не менее важным окажется способ, которым найден ответ. ИИ выступил не как калькулятор, а как система, построившая новый математический аргумент и доведшая его до формы, которую может проверить другой компьютер построчно.