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

Наприкінці 1930-х теореми Ґеделя про неповноту показали, що в будь-якій достатньо складній формальній системі є твердження, які не можна ні довести, ні спростувати всередині самої системи. Математичний світ тоді пережив методологічний шок: абсолютна повнота й несуперечність виявилися недосяжними ідеалами. Але сам процес перевірки доказів — хто, як і чому вірить теоремі — залишався зрозумілим: людина писала доказ, інші люди читали його й перевіряли крок за кроком.

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

Що конкретно каже Тао?

За даними The Decoder, Тао попереджає, що зростання обсягу й швидкості AI-генерованих доказів створює структурний розрив між тим, скільки контенту система здатна виробити, і тим, скільки рецензентів здатна виставити спільнота математиків. Рецензування — традиційний запобіжник математики — будувалося на припущенні, що доказ пишеться людиною в темпі, який інші люди встигають наздогнати. Коли темп генерації різко зростає, а автор доказу — модель, а не людина, це припущення перестає працювати.

Чим ця криза відрізняється від Ґеделевої?

Ґеделева криза була теоретичною: вона показала межі того, що взагалі можна довести. Криза, про яку попереджає Тао, — практична: питання не в тому, чи існує доказ, а в тому, чи можна йому довіряти, якщо ніхто фізично не встигає його перевірити. За нашою оцінкою, це принципово інша загроза — вона б'є не по фундаменту логіки, а по соціальному механізму, яким математика підтверджує істину: peer review. Якщо цей механізм захлинається обсягом, спільнота ризикує або уповільнити прийняття нових результатів до кризи, або почати приймати недоперевірені докази на віру.

Практичні наслідки такого розриву можуть включати:

Що це означає для AI-білдерів і формальної верифікації?

Питання довіри до AI-контенту виходить за межі коду — воно так само гостро стоїть і при формальній верифікації, де, здавалося б, є однозначний технічний арбітр: пруф-асистент на кшталт Lean чи Coq або перевіряє доказ, або ні. Але сама постановка задачі — формалізація твердження — усе одно проходить через людину чи модель, і помилка на цьому етапі не завжди видима перевірнику. Схожа логіка вже обговорювалася в контексті дистиляції моделей: якщо студент вчиться, не перевіряючи вчителя, помилки вчителя непомітно стають частиною знань учня — про це ми писали, розбираючи, чому сліпа довіра до моделі-вчителя небезпечна. У математиці роль «вчителя» зараз виконує AI-система, що генерує доказ, а роль «учня», якому бракує часу перевірити, — спільнота рецензентів.

Що з цим робити вже зараз?

Для команд, які будують AI-агентів для наукової чи інженерної роботи, висновок практичний: не сприймайте AI-згенерований доказ або код як фінальний артефакт — лише як чернетку, що потребує незалежної перевірки в детермінованому інструменті. Формальні верифікатори на кшталт Lean, Coq чи Isabelle залишаються найнадійнішим фільтром, бо не покладаються на людську увагу як вузьке місце. Окремий напрям — методи оцінки невпевненості моделі: якщо система здатна сама сигналізувати, у яких кроках доказу вона менш впевнена, оцінка невпевненості за один прохід може стати способом пріоритизувати, які фрагменти перевіряти людині в першу чергу, а не читати весь текст лінійно.

Висновок AiiN

Наша теза проста: криза, про яку каже Тао, — не проблема математики як окремої дисципліни, а перша велика ілюстрація загальнішого закону: коли швидкість генерації контенту AI обганяє швидкість людської перевірки, довіра переміщується з питання «хто це написав» на питання «чим це можна перевірити». Для галузей, де такого детермінованого верифікатора немає — більшість бізнес-логіки, юридичні висновки, медичні рекомендації, — ця криза настане раніше й буде тихішою: без Філдсівського лауреата, який публічно про неї попередить.

Хто такий Теренс Тао?

Теренс Тао — математик, професор Каліфорнійського університету в Лос-Анджелесі, лауреат Філдсівської медалі 2006 року за роботи в аналізі, теорії чисел і комбінаториці. Останні роки він відкрито експериментує з AI-інструментами й пруф-асистентами на кшталт Lean у колаборативних математичних проєктах.

Чим формальна верифікація відрізняється від рецензування?

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

Чи означає це, що AI не варто використовувати в математиці?

Ні — сам Тао активно використовує AI у власних проєктах формалізації. Проблема не в інструменті, а в тому, що інфраструктура перевірки — рецензенти, журнали, стандарти публікації — досі розрахована на темп людського письма, а не на темп генерації моделі.