Некоторые истины нельзя доказать принципиально: математики нашли пределы собственной реальности.

Исследователи, изучающие теорию вычислительной сложности, уже несколько десятилетий пытаются строго доказать то, что кажется интуитивно очевидным: существуют задачи, которые просто не поддаются эффективным алгоритмам. Об этом часто говорят на примере задачи коммивояжёра, где требуется найти кратчайший маршрут, проходящий через множество городов ровно один раз. На небольших входах эта игра выглядит безобидной, но по мере роста числа пунктов любые алгоритмы начинают «ломаться» под собственной вычислительной тяжестью. Специалисты уверены, что здесь нет скрытого быстрого решения, однако ни одно математическое доказательство этой уверенности пока не завершено.
И на фоне подобных трудностей всё больший интерес вызывает старая добрая метаматематика — область, которая исследует сами математические доказательства и те аксиомы, на которых они основаны. Логики пытаются понять не только то, какие утверждения можно вывести, но и где у самой системы рассуждений проходят границы. В теории сложности это особенно важно: если какое-то утверждение принципиально не вытекает из выбранных аксиом, то отсутствие доказательства перестаёт быть загадкой — это становится свойством математической вселенной, в которой работают исследователи. Поэтому учёные пересматривают наборы аксиом и проверяют, какие результаты становятся достижимыми при разных отправных точках.
В недавней работе трое исследователей воспользовались подходом, известным как «обратная математика». Он переворачивает привычный порядок: вместо того чтобы принять аксиомы и доказывать теорему, они подставили саму теорему на место аксиомы и проверили, можно ли из неё вывести исходное утверждение. Такой разворот позволил им показать, что ряд результатов из теории сложности, на первый взгляд никак не связанных друг с другом, в действительности обладают одинаковой логической силой в рамках выбранной системы. Само по себе это необычно: редко оказывается, что утверждения из разных областей стыкуются настолько точно.
Идея зародилась у Лицзе Чэня, который летом 2022 года, заканчивая диссертацию, решил посвятить время метаматематике. Он обратил внимание на задачу из коммуникационной сложности — области, изучающей, какое количество информации должны обменять два участника, чтобы решить совместную задачу. Один из классических примеров — определение равенства двух битовых строк при минимальном числе передаваемых сообщений. Уже давно известно, что природу этой задачи не обмануть: чтобы проверить совпадение, придётся переслать столько же битов, сколько содержится в строке. Это называется нижней границей — жёстким пределом, ниже которого никакому протоколу не опуститься.
Все известные доказательства этой нижней границы опираются на принцип Дирихле — фундаментальное утверждение, согласно которому множество объектов невозможно равномерно распределить по меньшему числу ячеек без повторов. Хотя этот принцип кажется школьной очевидностью, он играет огромную роль в комбинаторике и теории сложности. Чэнь заметил, что связь между задачей равенства и принципом Дирихле вполне может работать в обе стороны: если из принципа легко вывести нижнюю границу, то не получится ли, наоборот, вывести сам принцип, приняв нижнюю границу в качестве исходной посылки?
Совместно с Цзяту Ли он стал работать в логической системе PV1 — слабой, но удобной платформе для анализа связей между теоремами. Им удалось показать, что нижняя граница для задачи равенства и принцип Дирихле обладают одинаковой логической силой внутри этой системы: принимая одно утверждение как данность, можно вывести другое. Обсудив это с Игорем Оливейрой из Университета Уорика, исследователи пришли к выводу, что подобные связи могут существовать и между другими результатами теории сложности. Они начали проверять такие гипотезы одну за другой и обнаружили множество неожиданно эквивалентностей.
Самым ярким примером оказалась связь между принципом Дирихле и теоремой о минимальном времени, необходимом машине Тьюринга с одной лентой для проверки, является ли строка палиндромом. Эти две области выглядят несоизмеримыми: первое утверждение касается чистого счёта, второе — поведения абстрактной вычислительной машины. Однако внутри PV1 они оказываются равносильными. Удивление исследователей связано именно с тем, что такие теоремы обычно рассматриваются как слишком «узкие», специфичные, чтобы обладать фундаментальным статусом.
Новая сеть эквивалентностей помогает не только проследить скрытые связи между утверждениями, но и понять ограничения самой системы PV1. Если принцип Дирихле невозможно вывести без расширения аксиом, то все теоремы, оказывающиеся с ним логически эквивалентными, тоже недостижимы в рамках PV1. Это лишь усиливает представление о том, что попытки доказать фундаментальные границы могут упираться не в мастерство математиков, а в ограничения самих логических оснований, которые они используют.
Возможности обратной математики пока далеки от того, чтобы решить главные загадки теории сложности, но всё больше исследователей видят в ней шанс выбраться из тупика. Среди них и Цзяту Ли, который поступил в аспирантуру MIT и успел написать подробное руководство по метаматематике для специалистов по теории сложности. Интерес к теме растёт, и всё больше учёных готовы пересматривать аксиомы, от которых зависит судьба некоторых из самых известных нерешённых задач информатики.