Суперечливий математичний аргумент, який розділяв поле більше десяти років, нарешті може бути розв’язаний малоймовірним суддею: комп’ютерною програмою. Суть суперечки зосереджена навколо спроби Шінічі Мочізукі у 2012 році розв’язати гіпотезу ABC, давню проблему, яка глибоко вкорінена у фундаментальній природі чисел.
Гіпотеза ABC базується на надзвичайно простому рівнянні, що містить три цілі числа: a + b = c. Це включає в себе спеціальні правила, які регулюють, як прості числа, що складають ці цілі числа, повинні бути пов’язані одне з одним. Вирішення цієї, здавалося б, елементарної проблеми може відкрити глибоке розуміння галузі математики, потенційно вплинувши на інші відомі припущення, такі як остання теорема Ферма.
Мочізукі, професор Кіотського університету в Японії, представив свій аргумент у складній власній конструкції під назвою Міжуніверсальна теорія Тейхмюллера (IUT). Однак занадто технічний і незрозумілий характер теорії IUT для більшості математиків зробив її майже нечитабельною для тих, хто намагався перевірити його роботу. Початковий ентузіазм змінився розчаруванням, оскільки експерти боролися з його складними нюансами.
Підливаючи масла у вогонь, у 2018 році два видатних німецьких математики, Пітер Шольц і Якоб Стікс, виявили потенційний недолік у доказі Мочізукі. Мотідзукі заперечив їхні аргументи, і через відсутність загального органу для вирішення математичних суперечок поле розшарувалося на два табори: тих, хто в основному прийняв загальноприйнятий погляд (підтримуваний більшістю математиків), і меншу групу, що приєдналася до Мочізукі та його інституту в Кіото.
Зараз Мочізукі пропонує шлях вперед через формалізацію — перетворення свого доказу зі зрозумілої людині математичної нотації на Lean, мову програмування, спеціально розроблену для суворої математичної перевірки. Цей процес потенційно дозволить комп’ютерам автоматично перевіряти послідовність його аргументів, забезпечуючи безпрецедентний рівень об’єктивності.
Мочізукі вважає, що Lean має унікальні можливості для подолання складних мовних і концептуальних бар’єрів, які загальмували прогрес у розумінні теорії IUT. Він бачить це як інструмент для звільнення математичної істини від потенційних упереджень, притаманних людській інтерпретації.
Хоча деякі експерти, такі як Кевін Бадзард з Імперського коледжу Лондона, вважають це перспективним напрямком, вони також визнають величезну проблему, з якою він стикається. Формалізація теорії IUT вимагала б перекладу величезної маси складних рівнянь у ощадливий синтаксис, що можна порівняти з деякими з найбільших проектів формалізації, які будь-коли здійснювалися. Такі зусилля часто залучають цілі команди математиків і програмістів, на виконання яких потрібні місяці або навіть роки.
Йохан Коммелін з Утрехтського університету в Нідерландах, хоч і налаштований обережно оптимістично, наголошує, що успіх залежить від постійної відданості Мочізукі справі. Він попереджає, що якщо проект буде залишено передчасно, це може бути лише останнім епізодом довготривалої саги, позначеної невирішеними суперечками.
Навіть у разі успіху, зазначає Коммелін, навіть при комп’ютерній перевірці коду розбіжності щодо інтерпретації можуть зберігатися. Lean може вирішити логічні протиріччя, але це не обов’язково усуває всі філософські чи концептуальні розбіжності навколо роботи Мочізукі.
Зрештою, хоча формалізація дає проблиск надії на розв’язання цього вічного математичного протистояння, залишається відкритим питання, чи зможе вона подолати глибинні складності та різні точки зору, які характеризують дебати щодо доведення гіпотези ABC.
