Язык программирования, разработанный для надежной проверки математических теорем и выявления логических ошибок, был применен к научной статье по физике — и обнаружил ошибку. Это открытие поднимает вопрос о том, сколько еще статей могут содержать подобные проблемы.
Машины могут помочь выявить математические ошибки. Фото из архива Alamy
Созданный для выявления ошибок в математических теоремах компьютерный язык впервые обнаружил фундаментальную ошибку в широко цитируемой статье по физике. Исследователь, сделавший это открытие, говорит, что это первая статья по физике, которую он проанализировал таким образом, что поднимает тревожный вопрос: сколько еще статей содержат ошибки?
Для проверки правильности доказательств и отсутствия противоречий и логических пробелов все чаще используется специализированное программное обеспечение, применяемое в процессе, известном как формализация. Этот подход даже предлагается в качестве потенциального решения некоторых из самых сложных проблем в математике, таких как объемное (500 страниц) доказательство гипотезы ABC, представленное Синичи Мочизуки, по поводу которого эксперты спорят уже много лет.
Теперь Джозеф Туби-Смит из Университета Бата (Великобритания) применил язык формализации под названием Lean в области физики. Он попытался формализовать исследование, опубликованное в 2006 году, о стабильности потенциала модели двух дублетов Хиггса (2HDM), которое широко цитировалось в последующие годы, но случайно обнаружил ошибку, которая подрывает теорему.
Формализованные теоремы могут использоваться в качестве строительных блоков для формализации более сложных теорем, и Туби-Смит говорит, что его работа должна была стать «формальным заданием» для включения статьи в более крупный проект формализованных исследований в области физики под названием PhysLib, созданный по образцу существующей базы данных по математике под названием MathsLib. «Мы не стремимся опровергать существующие статьи; мы стремимся получить результаты, которые смогут использовать все», — говорит Туби-Смит.
Ошибка связана с утверждением, в котором авторы первоначальной работы говорят, что определённое условие C является достаточным для стабильного решения задачи. Однако Туби-Смит в ходе формализации показал, что существует условие C, которое не обеспечивает стабильного решения.
Туби-Смит говорит, что обнаружение ошибки оказывает существенное влияние на статью, но вряд ли вызовет проблемы в последующих работах, основанных на ней и цитируемых ею. Однако теперь он опасается, что многие статьи по физике содержат аналогичные ошибки, но не уверен, насколько широко распространена эта проблема. Он считает, что это убедительно доказывает необходимость формализации в качестве стандартной части публикации новых исследований.
Туби-Смит говорит, что физики, как правило, не приводят в теоремах столько подробных деталей, сколько математики. «Поскольку многих физиков не интересуют эти мельчайшие детали, иногда они их упускают, и именно здесь возникает ошибка», — говорит он.
Кевин Баззард из Имперского колледжа Лондона говорит, что формализация оказывает большое влияние на математику, и нет причин, по которым теоретическую физику, по крайней мере, нельзя рассматривать таким же образом. «Мы пытались заниматься математикой подобным образом, и это оказалось действительно интересным», — говорит он.
Однако реальная польза формализации в математике сейчас заключается в большом корпусе существующих формализованных теорем, что позволяет математикам легче развивать их, а также обучать модели ИИ, которые могут помочь быстрее формализовать новые теоремы. Обучение этих моделей ИИ для формализации математики требовало времени и множества конкретных примеров для использования в качестве обучающих данных, которые пока могут быть недоступны для физики.
«В идеале нам нужно миллион строк кода, описывающих физические процессы, и это может оказаться непростой задачей. Если машины изначально не очень хорошо справляются с физическими расчетами, то вначале придется выполнять ручную работу, а затем, будем надеяться, машины возьмут на себя эту задачу», — говорит Баззард.
Авторы оригинальной статьи по физике не ответили на запрос журнала New Scientist о комментариях, но Туби-Смит говорит, что сообщил им о своем открытии, получил подтверждение их согласия и ему сказали, что будет опубликовано исправление.
arXiv DOI: 10.48550/arXiv.2603.08139
Источник: www.newscientist.com
