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

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

Питання на мільйон: чи можна цей патерн — «генеруй з LLM, перевіряй ядром, що не вміє брехати» — перенести з чистої математики в код, криптографію і агентні системи, де ціна помилки не академічна, а виробнича? Відповідь часткова, і саме в нюансах цієї часткової відповіді ховається практична цінність новини.

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

Звідки взявся проєкт формалізації доведення Ферма?

Формалізація великих математичних доведень — окремий піджанр, старший за сучасний бум LLM років на п'ятнадцять. Ще 2012 року команда Жоржа Гонтьє в Coq завершила формалізацію теореми Фейта–Томпсон (255 сторінок оригінального доведення, класифікація скінченних груп непарного порядку) — робота зайняла шість років праці кількох дослідників. Томас Хейлз формалізував гіпотезу Кеплера в проєкті Flyspeck, витративши на це більше десяти років. Спільний знаменник цих проєктів простий: людина-формалізатор — головне вузьке місце. Перетворення природномовного математичного тексту в код, який приймає перевіряльник типів, — виснажлива, повільна робота, що вимагає одночасно глибокого знання предмета і формальної системи.

Доведення теореми Ферма — особливо складний кандидат для такої роботи, бо воно не самодостатнє: Вайлз спирається на гіпотезу Таніями–Шімури про модулярність еліптичних кривих, теорію представлень Галуа і десятки допоміжних результатів з алгебраїчної теорії чисел, розкиданих по інших роботах. Формалізувати саме доведення означає формалізувати значну частину сучасної алгебраїчної геометрії навколо нього — задача, яку математична спільнота Lean (бібліотека mathlib) обговорювала роками як «занадто велику, щоб братися». Поява LLM, здатних пропонувати правдоподібні тактики Lean і чернетки перекладу математичного тексту у формальні твердження, змінила розрахунок вартості: те, що вимагало команди формалізаторів на роки, стало можливим прискорити, розподіливши рутинні проміжні кроки між людьми та AI-асистентами.

Як це працює під капотом технічно?

В основі Lean лежить залежна типова теорія: кожне математичне твердження — це тип, а доведення цього твердження — терм цього типу. Ядро системи, яке перевіряє, що конкретний терм справді має заявлений тип, — навмисно крихітне, кілька тисяч рядків коду. Це критично: увесь mathlib, усі тактики, усі AI-згенеровані підказки можуть містити помилки, але фінальний вирок виносить саме це маленьке, ретельно перевірене ядро. Або доведення проходить перевірку типів, або система відмовляє його прийняти — компромісу «майже правильно» не існує.

AI-асистенти вбудовуються в цей процес у двох ролях. Перша — автоформалізація: переклад природномовного математичного тексту (статті Вайлза, підручники з теорії чисел) у формальні твердження мовою Lean. Модель пропонує чернетку формулювання, а математик перевіряє, що формальне твердження справді еквівалентне змістовному. Друга роль — синтез тактик: заповнення конкретних проміжних кроків доведення («sorry» — заглушок незавершених фрагментів) послідовностями тактик Lean, які модель підбирає, спираючись на корпус mathlib і контекст локальної цілі доведення.

Чому халюцинації тут не проблема

Ключова архітектурна деталь — цикл «згенеруй, потім перевір». Модель може запропонувати десять невдалих тактик поспіль, і це не коштує нічого, крім обчислень: ядро Lean миттєво відхилить кожну неправильну спробу, не пропустивши її як «правдоподібну». Це принципово інша економіка помилки порівняно зі звичайним чат-використанням LLM, де хибна відповідь спокійно йде користувачу. Тут модель по суті грає в дуже дорогий пошук навмання, але сам критерій успіху — не думка іншої моделі чи людини, а формальна перевірка типів.

Чим це відрізняється від AlphaProof та інших підходів?

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

Раніший підхід GPT-f та методика Draft-Sketch-Prove (напрацьована дослідниками з формальних методів у 2020–2022 роках) першими показали схему «модель накидає ескіз доведення, автоматичні доводчики заповнюють деталі» — саме з неї виріс сучасний патерн автоформалізації. Класичніший інструмент, Sledgehammer в Isabelle/HOL, взагалі не використовує LLM — він перебирає класичні автоматичні доводчики теорем (ATP) і працює непогано для локальних, «технічних» кроків, але спотикається на творчих стрибках, які потрібні у великих доведеннях на кшталт Ферма.

Головна відмінність нинішнього проєкту від Feit–Thompson і Flyspeck — не в методі перевірки (Lean замість Coq/HOL Light), а в співвідношенні людини й машини всередині процесу: команда формалізаторів більше не пише кожну тактику вручну, а курує й перевіряє те, що згенерував AI-асистент, зосереджуючи людську увагу на постановці правильних проміжних тверджень, а не на механічному підборі синтаксису доведення.

Що це дає тим, хто будує на цьому вже зараз?

Практична цінність тут не в математиці, а в патерні. Три сценарії, де він уже застосовний поза академією:

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

Чого тут не вистачає і що може піти не так?

Найбільша практична пастка — не в самому ядрі перевірки, а на етапі автоформалізації. LLM може перекласти змістовне математичне твердження в синтаксично коректне формальне твердження, яке проходить перевірку типів, але означає не зовсім те, що малося на увазі — класична проблема «formalization gap». Ядро Lean підтвердить, що доведений саме той (неправильно сформульований) вираз, і жодна автоматична перевірка це не спіймає: потрібне експертне читання постановки задачі людиною. Тобто вузьке місце не зникає, воно зсувається — з написання тактик на верифікацію специфікацій.

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

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

Висновок AiiN

Ми в AiiN розглядаємо формалізацію доведення Ферма не як математичну новину, а як публічний доказ концепції для патерну «генеруй LLM-ом, перевіряй незалежним детермінованим ядром» — того самого, який має найбільше шансів вирішити проблему довіри до AI-виводу в найближчі роки, і саме тому вважаємо його вартим уваги інженерів, що ніколи не відкриють підручник з алгебраїчної геометрії. На горизонті 6–12 місяців очікуємо не проривів у відкритті нової математики, а тихішу, практичнішу хвилю: більше анонсів AI-асистованої формалізації криптобібліотек і компіляторних доведень, зрілі інструменти пошуку по mathlib для LLM-агентів, і появу подібних generate-and-verify пайплайнів у продуктовому коді — там, де вже є тести, типи чи специфікації, здатні відіграти роль ядра Lean. Порада практикам: якщо у вашому домені є хоч якийсь детермінований перевіряльник істини, саме зараз час проєктувати навколо нього агентний цикл, а не навколо довіри до сирого виводу моделі.

Поширені питання

Чи означає це, що AI тепер вміє самостійно доводити нові теореми? Ні. Формалізація Ферма — це переклад і верифікація вже існуючого людського доведення, а не самостійне відкриття нового результату; автономний пошук нових доведень (як у AlphaProof) поки обмежений компактними, самодостатніми задачами олімпіадного рівня.

Чи можна застосувати цей підхід поза математикою? Так, і саме тут найближча практична вигода: формальна верифікація коду, криптопротоколів і смарт-контрактів структурно ідентична задачі — потрібен лише детермінований перевіряльник, яким може бути компілятор, набір тестів або формальна специфікація замість ядра Lean.