Появилась новая статья о формализации квантовой теории поля (КТП), в которой утверждается, что КТП формализована с использованием Lean/Mathlib. Я старался избегать погружения в актуальные темы, связанные с искусственным интеллектом и доказательством теорем, но в данном случае многое пересекается с тем, о чём я думал в последнее время (и писал об этом в своём блоге, см. эту публикацию).
Авторы работают над этим с июля прошлого года, и вы можете ознакомиться с методами, которые они использовали, в разделе 5 их статьи. Теорема, которую они доказывают, заключается в том, что если вы начнёте с обычной двухточечной функции Швингера свободного скалярного поля…
Основная проблема с любыми утверждениями о «формализации КТП» заключается в том, что у нас фактически нет принятого определения того, что такое КТП. Авторы берут определение из книги Глимма и Джейффе: вероятностная мера на распределениях, удовлетворяющая пяти аксиомам, обозначенным как OS0–OS4. Им нужно проделать большую работу, чтобы формализовать доказательство того, что можно построить меру с такими свойствами из $K(x,y)$. Однако такое доказательство является довольно стандартным и хорошо понятным уже давно. Это не та тема, где есть опасения, что могут возникнуть какие-то тонкие проблемы.
Очевидный вопрос: почему использовать это определение Глимма и Джейффе для КТП? Использование «OS» относится к оригинальной работе по характеристике евклидовых КТП Остервальдера — Шрадера. Если вы посмотрите их статью, они характеризуют евклидову КТП как набор функций Швингера, удовлетворяющих набору аксиом E0–E4 (они намеревались показать, что после преобразования Вика они подразумевают обычные аксиомы Вайтмана). В статье Остервальдера и Шрадера ничего не говорится о мерах, и хотя их аксиомы соответствуют аксиомам Глимма и Джейффе, они отличаются.
Почему бы не формализовать свободное скалярное КТП, используя определение Остервальдера — Шрадера для евклидовой КТП? Причина, я думаю, в том, что это было бы слишком просто: единственная аксиома, которой свободные функции Швингера не удовлетворяют очевидным образом, — это аксиома положительности (признание значимости этого было большим вкладом Остервальдера и Шрадера). Аргумент в пользу положительности свободной теории по Остервальдеру — Шрадеру прост, но показывает, что происходит нечто довольно интересное (я потратил немало времени, пытаясь понять это в терминах гиперфункций).
Почти вся работа в этой конкретной формализации сводится к тому, чтобы поместить КТП свободного поля в определённую теоретико-измерительную «пряжку». Эта «пряжка» подходит только для КТП реального скалярного поля, возможно, с самовзаимодействиями, но не применяется к КТП, имеющим отношение к фундаментальной физике (калибровочные поля, фермионные спинорные поля, калибровочные взаимодействия).
Интересно, что этот класс КТП по сути является статистико-механическими системами и может быть изучен с помощью методов теории вероятностей. Проблема в том, что они не только не соответствуют никаким фундаментальным КТП реального мира, но и единственные нетривиальные примеры существуют в двух и трёх измерениях пространства-времени. Теперь у нас есть доказательства того, что если вы попытаетесь сделать это в четырёх и более измерениях пространства-времени, вы сможете получить только теорию свободного поля.
Авторы осознают это и в качестве мотивации утверждают, что формализуют теорию Янга — Миллса. К настоящему времени существует 50-летняя история попыток людей следовать этой программе построения некоторой меры на калибровочных полях, демонстрации массового разрыва и получения миллиона долларов, но я не вижу никаких доказательств того, что это куда-то приведёт. Наверняка нужны новые, совершенно другие идеи. Они также утверждают, что в качестве мотивации создают меру на метриках, которая дала бы квантовую гравитацию, но опять же пятьдесят лет попыток людей сделать это указывают на то, что это не очень хорошая отправная точка.
Для дальнейшего прогресса, скорее всего, потребуется то же самое, что почти всегда необходимо для большого прорыва, когда область застряла на десятилетия: изменение вопроса. В данном случае нужно другое определение КТП, чем мера на пространстве распределений. Поиск этого нового определения — интересная задача, а не повторное доказательство хорошо известных следствий определения, которое, как вы знаете, неверно.
Программа искусственного интеллекта и формализации, которую нам продают как будущее фундаментальной физики, на мой взгляд, сопряжена с большой опасностью. Она может превратить эту область в не что иное, как бесконечное исследование тупиковых путей, которыми мы располагаем сейчас и в которых застряли на десятилетия. Эта конкретная «формализация КТП» — экспедиция, возглавляемая в такой тупик.