Компьютерный алгоритм впервые выявил фундаментальную ошибку в известной статье по физике
Этот прецедент вызвал в научном сообществе дискуссии о том, сколько еще опубликованных исследований могут содержать подобные скрытые недочеты.
Исследователь Джозеф Туби-Смит из Университета Бата (Великобритания) применил язык формализации Lean для анализа статьи 2006 года, посвященной стабильности потенциала модели двух хиггсовских дублетов.
В ходе проверки алгоритм выявил логическое противоречие: авторы оригинальной публикации утверждали, что определенное условие C является достаточным для обеспечения стабильного решения проблемы. Однако компьютерный анализ доказал, что существует вариант этого условия, при котором стабильное решение невозможно, что фактически разрушает предложенную в статье теорему.
По словам Туби-Смита, он не ставил перед собой цель опровергнуть чью-либо работу. Проверка проводилась в рамках рутинного переноса данных в PhysLib — новую цифровую библиотеку формализованных физических исследований, создаваемую по образу уже существующей математической базы MathsLib.
Хотя обнаруженная ошибка нивелирует конкретную теорему, ученый считает маловероятным, что она критически повлияет на последующие научные труды, которые цитировали эту статью. Тем не менее, исследователь опасается, что из-за разницы в подходах многие другие работы по физике могут содержать аналогичные скрытые ошибки.
В отличие от математиков, физики часто опускают мельчайшие технические детали в своих доказательствах, что и создает почву для неточностей. В связи с этим Туби-Смит выступает за внедрение обязательной компьютерной формализации как стандарта при публикации новых физических исследований.
Программное обеспечение для формализации уже доказало свою эффективность в математике, помогая ученым проверять гигантские труды на предмет противоречий (например, 500-страничное доказательство abc-гипотезы Синъити Мотидзуки). Однако главной проблемой на данный момент является отсутствие в физике такой же обширной базы уже переведенных в машинный код теорем, какая есть в математике.
Авторы оригинальной публикации 2006 года уже уведомлены об обнаруженном недочете. Они согласились с выводами Джозефа Туби-Смита и подтвердили намерение выпустить официальное исправление к своей статье.
Залогиньтесь, чтобы писать комментарии