Великую теорему Ферма докажут по второму кругу: что не так с первым доказательством

Великая теорема Ферма мучила математиков на протяжении веков, пока не была окончательно доказана в 1993 году. Теперь же ученые хотят получить версию доказательства, которую можно было бы формально проверить с помощью компьютера на наличие любых логических ошибок, пишет New Scientist.

В планах у исследователей, разработать компьютеризированное доказательство Великой теоремы Ферма. Согласно теореме Пьера де Ферма, которую он впервые вывел около 1640 года, утверждает, что при значениях n > 2 уравнения вида xn + yn = zn не имеют ненулевых решений в натуральных числах.

У Фокус.Технологии появился свой Telegram-канал. Подписывайтесь, чтобы не пропускать самые свежие и захватывающие новости из мира науки!

Только в 1993 году Эндрю Уайлс, который работа в Принстонском университете, заявил, что вывел доказательство. Оно занимало более 100 страниц и включало настолько сложную математику, что коллегам Уайлса понадобилось более 2 лет, чтобы убедиться, что доказательство не ошибочно.

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

Кевин Баззард из Имперского колледжа Лондона и его коллеги объявили о своих планах попытаться формализировать Великую теорему Ферма на языке программирования под названием Lean.

"В Великой теореме Ферма нет никакого смысла, она совершенно бесполезна. У нее нет никакого применения – ни теоретического, ни практического – здесь, в реальном мире. Но она важна, так как на протяжении веков люди генерировали множество блестящих новых идей, пытая доказать теорему", — говорит Баззард.

"Этот проект может иметь далеко идущие и неожиданные преимущества и по следствия", — отметил Крис Уильямс из Ноттингемского университета.

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

Напомним, ученые использовали теорему 350-летней давности, чтобы обнаружить новые свойства света. Новое исследование выявило неизвестные ранее связи между некоторыми наиболее загадочными свойствами света.