Цифрова верифікація: чи зможуть комп’ютери дозволити найбільший глухий кут у математиці?
Вже понад десять років математична спільнота веде запеклі суперечки про справжність одного масштабного і вкрай спірного доказу. Сьогодні на передній план виходить нова технологічна область — комп’ютерна формалізація, яка пропонує потенційний спосіб нарешті вирішити цю суперечку.
Конфлікт навколо гіпотези ABC
У центрі конфлікту знаходиться гіпотеза ABC — фундаментальна проблема, що стосується взаємозв’язку між додаванням та множенням простих чисел. У 2012 році Сіньйіті Мотідзукі з Кіотського університету опублікував 500-сторінковий доказ, який претендує на вирішення цієї давньої загадки.
Однак його метод — найскладніша теоретична база, звана міжуніверсальною теорією Тейхмюллера (IUT), виявився настільки безпрецедентним, що розділив світову математичну спільноту. У той час як Мотідзукі та його прихильники наполягають на правильності доказу, багато видатних математиків, включаючи Пітера Шольце та Якоба Стікса, стверджують, що в логіці міститься фатальна помилка.
Цей глухий кут створив рідкісний для сучасної науки стан «патової ситуації»: одна сторона бачить у роботі проривну істину, тоді як інша — нерозбірливі чи помилкові міркування.
Розквіт формалізації
Щоб вийти із цього замкнутого кола, дослідники звертаються до Lean — спеціалізованої мови програмування, призначеної для «формалізації». У цьому процесі математичні докази перекладаються кодом, який комп’ютер може перевірити з абсолютною логічною достовірністю. Це виключає «людський фактор» — можливість недорозуміння, соціального тиску чи упередженості під час рецензування — і замінює його бінарною істиною.
В даний час два різні проекти намагаються використовувати цю технологію, щоб поставити крапку в цьому питанні:
1. Проект LANA (Пошук істини)
Під керівництвом Фуміхар Като з математичного центру ZEN, проект «Lean and Anabelian geometry» (LANA) прагне верифікувати доказ раз і назавжди. До цієї групи входять експерти як за специфічними теоріями Мотідзукі, так і з мови програмування Lean.
Незважаючи на досягнутий прогрес, проект зіткнувся із серйозною перешкодою. Вони виявили в теорії IUT конкретний проблемний момент, який дзеркально відображає помилку, виявлену Шольце та Стіксом у 2018 році. Після вісімнадцяти місяців інтенсивного вивчення команда ще не може розплутати цей логічний вузол.
2. Проект Мотідзукі (Пошук ясності)
Використовуючи інший підхід, Мотідзукі та його колеги також почали формалізувати свою роботу мовою Lean. Проте їхня мета — не «довести» власну правоту (оскільки вони вважають її вже встановленою), а використовувати код як інструмент точної комунікації.
Мотидзукі стверджує, що Lean створить «точний запис» його логічної структури, що зробить її невразливою для невірних інтерпретацій, які підживлювали роками полеміку. Хоча його команда вже створила перші 70 рядків коду, експерти зазначають, що це лише початок колосальної роботи.
Чому це важливо
Вирішення питання з гіпотезою ABC – це не просто питання одного рівняння; це поворотний момент у самій практиці математики.
- Криза верифікації: Якщо комп’ютер виявить помилку, це покладе край десятиріччю академічних тертя.
- Нова методологія: Якщо доказ підтвердиться, це доведе, що «формалізація» є життєздатним способом роботи з математичними ідеями, складність яких перевищує когнітивні межі людини.
- Міст для комунікації: Діалог між проектом LANA та групою Мотідзукі показує, що технології можуть нарешті надати спільну мову математикам, які інакше не здатні ефективно спілкуватися один з одним.
Висновок
Незважаючи на величезні технічні труднощі, перехід до математики, що перевіряється комп’ютерами, є першим реальним рухом у суперечці навколо гіпотези ABC за багато років. Чи підтвердить код Мотидзукі роботу чи виправить її, результат фундаментально змінить способи встановлення та передачі математичної істини.
