Наближення до точки колапсу зумовлене зростаючою складністю математичних доведень та швидкістю, з якою штучний інтелект (ШІ) генерує потенційні рішення. Приклади, такі як доведення Пуанкаре чи гіпотези Рімана, вимагають значних людських зусиль для верифікації, що стає майже неможливим при масовому генеруванні доведень ШІ. Більше того, сама природа тренування ШІ на даних, створених людьми, призводить до інкорпорації людських упереджень та помилок у майбутні наукові відкриття, роблячи людину основним вузьким місцем у процесі перевірки.
Криза верифікації та роль штучного інтелекту
Історично, вирішення складних математичних проблем, як-от гіпотеза Пуанкаре, потребувало тривалої роботи окремих математиків та колективних зусиль наукової спільноти для перевірки. Доведення Вейлса теореми Ферма також наочно продемонструвало, як одна помилка може призвести до руйнування цілісного доказу, вимагаючи значних додаткових зусиль для його виправлення. Нині ШІ, що колись ледь міг вирішувати базові завдання, тепер демонструє здатність конкурувати на рівні міжнародних олімпіад. Однак, час, необхідний ШІ для генерації рішення, значно менший за час, який експерт-людина витрачає на його перевірку. З огляду на експоненційне зростання можливостей ШІ, очікується, що незабаром ми зіткнемося з тисячами доведень, які людський ресурс не зможе верифікувати, зокрема, щодо фундаментальних проблем, таких як гіпотеза Рімана чи P проти NP.
Крім того, процес навчання ШІ на основі інтернет-даних означає, що система може успадкувати та масштабувати людські когнітивні упередження та помилки. Це ставить під загрозу надійність майбутніх математичних відкриттів, викликаючи питання про те, чи не стаємо ми залежними від неперевірених тверджень, втрачаючи потенціал ШІ для революції в математиці.
Формальна математика як ключ до нової ери
Відповіддю на ці виклики є перехід до формальної математики – мови, зрозумілої для комп'ютерів. Ця ідея має глибоке історичне коріння, починаючи з бачення Готфріда Вільгельма Лейбніца у XVII столітті. Лейбніц мріяв про універсальну систему, яка б об'єднувала логічну мову, енциклопедію перевірених знань та «механізм розуму» для автоматичного виведення нових істин. Хоча його амбіції потребували століть для реалізації, сучасні технології роблять це можливим.
Сучасна реалізація цієї візії включає три ключові компоненти: мова програмування Lean, яка функціонує як асистент доведень, перевіряючи не лише синтаксис, але й логічну сутність математичних аргументів; Mathlib – відкритий проєкт, що містить мільйони рядків коду Lean і є своєрідною «Вікіпедією» математичних фактів, де кожне твердження перевіряється обчислювально; та, власне, роль штучного інтелекту як «механізму розуму».
Майбутнє математичних досліджень полягає у створенні доведень мовою Lean, що дозволить комп'ютерам автоматично верифікувати їх з абсолютною точністю. Це трансформує роль людини: від детального перевіряльника до творця гіпотез, що формулює напрямки досліджень. ШІ стане надійним партнером, здатним досліджувати величезні логічні простори та надавати перевірені результати. Вже цього року на Міжнародній олімпіаді з математики автоматизовані системи знайшли розв'язки для п'яти з шести завдань у формі, що не потребує людської верифікації, демонструючи рівень золотих медалістів.
Таким чином, людство стоїть на порозі нової ери математичних відкриттів, де партнерство між людською інтуїцією та надлюдським математичним інтелектом, підкріплене формальною верифікацією, відкриє нові горизонти пізнання.