Велику теорему Ферма доведуть по другому колу: що не так із першим доказом

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

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

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

Лише 1993 року Ендрю Вайлс, який працював у Принстонському університеті, заявив, що вивів доказ. Він займав понад 100 сторінок і включав настільки складну математику, що колегам Вайлса знадобилося понад 2 роки, щоб переконатися, що доказ не помилковий.

У сучасному світі математики вважають, що роботу з перевірки, а можливо навіть, виведення доказів можна прискорити, якщо перекласти теорему на мову комп'ютерів. Такий процес формалізації дасть змогу комп'ютерам миттєво знаходити логічні помилки, а також використовувати будівельні блоки теореми для доказів інших.

Кевін Баззард з Імперського коледжу Лондона і його колеги оголосили про свої плани спробувати формалізувати Велику теорему Ферма мовою програмування під назвою Lean.

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

"Цей проєкт може мати далекосяжні й несподівані переваги та наслідки", — зазначив Кріс Вільямс із Ноттінгемського університету.

За словами дослідників, доказ теореми мовою програмування буде слідувати методу Вайлса, але з невеликими змінами. Загальнодоступний проєкт буде доступний в інтернеті, щойно проєкт запустять у квітні, тож будь-хто зі швидкозростаючої спільноти Lean зможе зробити свій внесок у формалізацію розділів доказу.

Нагадаємо, вчені використовували теорему 350-річної давнини, щоб виявити нові властивості світла. Нове дослідження виявило невідомі раніше зв'язки між деякими найбільш загадковими властивостями світла.