Асистент доведення Lean і ШІ: як докази стають машинно перевірюваними

Одинадцять днів, рій агентів, 13 мільйонів рядків коду: ШІ зробив доведення останньої теореми Ферма машинно перевірюваним. Вирішальною була не стільки обчислювальна потужність, скільки перевіряльник, який не пропускає жодної помилки.

Близько 1637 року П'єр де Ферма записав на березі книги твердження, для якого нібито мав доведення. Його так і не знайшли. Лише 1995 року Ендрю Вайлс опублікував повне доведення. 4 вересня 2026 року Anthropic повідомила, що рій агентів Claude повністю формалізував це доведення мовою Lean. Це стало можливим завдяки асистенту доведення Lean, який машинно перевіряє кожен крок доведення.

Ця стаття розглядає це повідомлення в контексті. Вона пояснює, що таке асистент доведення і чому результату з Lean можна довіряти. Описує, як співпрацювали агенти, і ставить повідомлення в один ряд із олімпіадними задачами та проблемами Ердеша. При цьому підтверджені цифри, заяви виробника та відкриті питання розділено. Теза: новим є не лише те, що ШІ працює з математикою. Нове в поєднанні моделі, якій дозволено вільно пробувати, і програми, яка бездоганно приймає кожен крок.

Остання теорема Ферма: що саме повідомила Anthropic

Теорема стверджує, що рівняння aⁿ + bⁿ = cⁿ не має розв'язків у цілих числах, більших за нуль, при показнику n більше 2. Твердження легко зрозуміти, а доводити його століттями було надзвичайно важко. 1908 року призначили премію в 100 000 золотих марок, і, за даними Anthropic, за перший рік надійшло 621 хибне доведення. Вайлс представив доведення 1993 року, виявив прогалину й закрив її разом із Річардом Тейлором. Публікація вийшла в травні 1995 року.

Нове повідомлення стосується питання, наскільки надійне це доведення, коли кожен крок перевіряє машина. Ключові дані з публікації Anthropic наведено в таблиці.

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

Важливе розмежування. Йдеться про формалізацію, а не про нове доведення. Теорему доведено ще 1995 року. Агенти, за даними Anthropic, спиралися на спрощену версію доведення Вайлса за авторства Дармона, Даймонда і Тейлора та взяли частини з проєкту формалізації Імперського коледжу й проєкту flt-regular. Тож хто читає про розв'язання теореми Ферма за допомогою ШІ, має думати не про нове математичне відкриття, а про верифікацію. Anthropic прямо відмежовує цей результат від роботи ШІ над гіпотезою Рімана, де, за її словами, було відкрито щось нове.

Що таке Lean? Асистент доведення, який не пропускає жодного кроку

Асистент доведення Lean — це відкрита мова програмування, якою математичні доведення можна записати так, щоб їх міг перевірити комп'ютер. Сторінка проєкту lean-lang.org описує Lean як мову програмування й асистент доведення з мінімальним довіреним ядром, що гарантує коректність. Lean розробив Леонардо де Моура, а 2013 року його опубліковано як відкритий код, як повідомляє Simons Foundation. З 2023 року над розвитком працює неприбуткова Lean FRO, яку підтримує, зокрема, Simons Foundation International сумою 5 мільйонів доларів США.

Принцип можна пояснити простою мовою. Доведення в Lean — це програма. Ядро Lean крок за кроком перевіряє, чи кожен висновок випливає з аксіом і вже перевірених теорем. Аксіоми — це основні припущення математики, що приймаються без доведення. Крок, який не випливає, відхиляється, хоч би яким переконливим він звучав. Там, де доведення ще бракує, у Lean стоїть заповнювач «sorry». Доведення з такими заповнювачами вважається неповним.

Саме це робить Lean таким корисним для моделей ШІ. Мовні моделі можуть переконливо формулювати і при цьому помилятися. У математиці це проблема, адже помилка на кроці 400 може знецінити все, що після неї. З асистентом доведення на кшталт Lean питання, чи можна вірити моделі, відпадає.

Рецензування людьми працює інакше. Фахівці читають доведення, вважають його правдоподібним і покладаються на свій досвід. Це цінно, але потребує часу й залишає простір для недогляду. Ще 2021 року спільний проєкт у Lean валідував складне доведення Пітера Шольце, як описує Simons Foundation. Перевірка асистентом доведення не замінює математичного розуміння, але дає впевненість у коректності.

Процес на рисунку 1 показує розподіл праці: модель пропонує, ядро Lean виносить вирок. Чи походить пропозиція від людини, моделі чи генератора випадкових чисел, для вироку значення не має.

Mathlib і питання, хто перевіряє те, що перевірено

Сам по собі Lean ще не містить математики. Вона міститься в Mathlib, спільно розроблюваній бібліотеці, на якій ґрунтуються майже всі формалізації. Сторінка Lean називає понад мільйон рядків. Сторінка статистики спільноти на момент відкриття показувала 139 391 означення, 290 502 теореми та 772 учасники. Хто щось доводить у Lean, може спиратися на ці перевірені будівельні блоки, а не починати з нуля.

Для порівняння: доведення теореми Ферма, за даними Anthropic, має близько 13 мільйонів рядків і тим самим більш ніж у п'ять разів більше за Mathlib. Це звучить як величезне нове будівництво, але також показує, скільки коштує формальна верифікація глибоких теорем, навіть коли Mathlib дає основу. Доведення залежить від того, що вже формалізовано в Mathlib.

Слід ставити два окремі питання перевірки. По-перше: чи коректне доведення? Це вирішує Lean. Anthropic зазначає, що використовуються лише три стандартні аксіоми. По-друге: чи справді доведено теорему Ферма, а не змінене твердження? Тут застосовано інструмент Comparator, який підтвердив, що формалізоване твердження збігається з формулюванням у Mathlib. Це розмежування вирішальне. Безпомилкове доведення хибного твердження було б марним.

Повне доведення, за даними Anthropic, разом із письмовим поясненням лежить на GitHub і доступне для перегляду. Непублічною є лише використана модель.

Кевін Баззард з Імперського коледжу Лондона, який очолює проєкт формалізації з 2024 року, перевірив доведення. За даними Anthropic, він зазначає, що теорему доведено без припущень, окрім аксіом математики. Одна межа залишається: Lean перевіряє коректність, а не зміст. Чи є результат цікавим, елегантним або важливим, інструмент не оцінює. Відповідні оцінки Алекса Конторовича наводить Simons Foundation.

Агентний ШІ: чому рій спрацював

Паралельно працювало кілька десятків агентів. Агент у цьому контексті — це мовна модель, яка не лише відповідає, а й самостійно використовує інструменти, редагує файли та перевіряє проміжні результати. Каркас для багатьох агентів ґрунтувався на Claude Code. Агенти визначали поняття, доводили проміжні теореми й використовували їх для складніших тверджень. Загальне введення пропонує стаття Das Zeitalter der KI-Agenten.

Прорив, за словами Anthropic, забезпечила не потужніша модель, а краща організація. Платформа Prove2Me, відкрита платформа співпраці Тяньї Пена та колег із Колумбійського університету, пропонувала три властивості:

• Орієнтиром слугував спрямований ациклічний граф тверджень теорем: кожне твердження показує, від чого воно залежить, і циклів немає.
• Твердження й доведення лежали в окремих файлах. Це пришвидшує компіляцію Lean, бо не потрібно щоразу перевіряти все заново.
• Уже доведені теореми можна було шукати й повторно використовувати за описами природною мовою.

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

Участь людини була невеликою, але не нульовою. Тяньї Пен час від часу давав вказівки вищого рівня, наприклад пріоритезувати якобіан як схему або найближчим часом завершити теорему Мазура. Згідно з наведеним виводом агентів, система повідомила про доведення кореневого результату 18 серпня о 02:00:57 UTC.

Від олімпіади до проблем Ердеша: докази ШІ з 2024 року

Повідомлення про Ферма не поодиноке. З 2024 року кілька результатів показують, що ШІ може доводити математичні твердження, і вони відрізняються тим, чи використовувався Lean.

У липні 2024 року AlphaProof разом з AlphaGeometry 2 розв'язав чотири із шести задач Міжнародної математичної олімпіади й набрав 28 із 42 балів, рівень срібла. Межа золота становила 29 балів. AlphaProof доводить у Lean і розв'язав, зокрема, найскладнішу задачу змагання. Проте задачі спершу вручну перекладали формальною мовою, а час обчислень становив до трьох днів на задачу. Учасники мають двічі по 4,5 години.

У липні 2025 року Gemini Deep Think набрав 35 із 42 балів, рівень золота, офіційно оцінений координаторами олімпіади. Система працювала природною мовою в межах часового ліміту і без Lean. Це свідомий контраст: ШІ сильний і без формальної перевірки, але тоді результати не верифіковані машинно, їх мають читати люди. Компанія Harmonic описує в публікації на arXiv свою систему Aristotle, що поєднує пошук доведень на основі Lean з неформальними міркуваннями та розв'язувачем геометрії і, за анотацією, досягає рівня золота на задачах 2025 року.

На початку 2026 року в центр уваги потрапили проблеми Ердеша, велика збірка відкритих питань математика Пола Ердеша. Один із прикладів — проблема 728, доведення якої від Aristotle у Lean задокументоване як виклад на arXiv. За даними Simons Foundation, 23-річний юнак на початку 2026 року також розв'язав проблему 1196 за допомогою ChatGPT і Lean.

Оцінка обережна. Вікі Теренса Тао про внески ШІ в проблеми Ердеша прямо не вважає себе бенчмарком. Воно називає упередженість відбору, бо успіхи документують охочіше за невдачі. Воно вказує, що відсутність попереднього прогресу часто свідчить про невідомість, а не про складність, що згодом нерідко знаходилася вже наявна література і що розв'язана проблема не обов'язково є роботою, готовою до публікації. Водночас вікі радить формально перевіряти докази ШІ в Lean.

Сфера доведень ШІ в математиці охоплює змагальні задачі, периферійні проблеми та великі формалізації. Розвиток іде швидко; чи кожне повідомлення виправдовує заголовок, треба перевіряти окремо. Саме для цього призначений інструмент перевірки на кшталт Lean.

Скільки варті 11 днів? Порівняння часу без перебільшень

Ці цифри спокушають на гучні порівняння. Ферма сформулював теорему 1637 року, Вайлс довів її 1995 року, це 358 років. Проєкт формалізації в Імперському коледжі стартував 2024 року з blueprint на 86 сторінок і спочатку був розрахований на кілька років. Формалізація за допомогою ШІ тривала 11 днів.

Це зіставлення кульгає з кількох причин:

• 11 днів — це час роботи рою агентів, а не обчислювальний час однієї моделі.
• Доведення було відоме. ШІ не мав знаходити нову ідею, а лише перекласти наявну структуру доведення в Lean.
• Була попередня робота: Mathlib, матеріали з проєкту Імперського коледжу та flt-regular, а також blueprint.
• Витрати близько шести мільярдів вихідних токенів внутрішньої моделі значні. Вартість у грошах не вказана.

Прирівнювання 11 днів роботи ШІ до століть людської праці над проблемою тому є лише риторичним порівнянням. Правильно інше: роботу, яку спільний проєкт планував на роки, по суті завершили за кілька днів.

Побічний експеримент спрямовує погляд на повсякденність. За даними Anthropic, три особисті підписки Claude Max за три дні формалізували теорему Виноградова про три прості числа. Автори вважають спільну формалізацію зі споживчими підписками можливою, якщо каркас правильний. Це оцінка авторів, а не незалежно підтверджений результат.

Межі та відкриті питання: чого повідомлення не показує

Anthropic сама називає обмеження. Доведення, імовірно, значно довше, ніж потрібно, адже Mathlib компактніший і краще перевірений. Воно залежить від того, що вже формалізовано в Mathlib. Використана модель — внутрішня, непублічна дослідницька, тож результат не можна повторити ззовні тими самими засобами.

Інші пункти лишаються відкритими:

• Нової математики не створено. Формалізація підвищує певність, а не знання.
• Доведення в Lean не є автоматично зрозумілим. 13 мільйонів рядків ніхто не прочитає від початку до кінця.
• Lean нічого не каже про значущість теореми, а лише про її коректність.
• Наскільки незалежною є перевірка поза оцінкою Баззарда, із повідомлення не видно.

Щодо інших окремих повідомлень, наприклад про поліпшення в гіпотезі Рімана чи про агентів автоформалізації окремих компаній, у цьому дослідженні немає первинних джерел, які можна було б самостійно перевірити. Тому ці повідомлення тут подано без цифр. Оцінки окремих фахівців також беруться лише тоді, коли є оригінальна заява.

Що підхід Lean означає поза математикою

Модель, що стоїть за проєктом Ферма, можна узагальнити: вільне пробування з одного боку, жорстке приймання з іншого. Вона підходить скрізь, де результат можна перевірити машинно. Сторінка Lean називає як застосування поза математикою верифікацію ArkLib, бібліотеки про SNARK (компактні криптографічні докази), та Cedar, мови авторизації AWS. У розробці програмного забезпечення цей принцип відомий: компілятор і тестовий прогін так само приймають те, що написала людина чи ШІ.

Для поводження з виводом ШІ звідси випливає практичне правило. Чим краще результат піддається автоматичній перевірці, тим безпечніше модель може працювати вільно. Для текстів, оцінок і рекомендацій такого жорсткого приймання зазвичай немає. Там перевіряльником лишається людина.

Та сама логіка діє для безпеки та захисту даних: доказувані властивості важать більше за прості твердження. Чи завантажує вебсайт трекери або чи встановлює заголовки безпеки, можна виміряти автоматично. Для цього Webseiten-Check від Dr. DSGVO пропонує можливість, а технічні властивості безпеки можна перевірити за допомогою Security-Checks. Обидва не є формальними доведеннями в сенсі Lean, але дотримуються тієї самої ідеї: вимірювати, а не вірити.

Експерименти Dr. DSGVO

За допомогою ШІ (імовірно) отримано та формалізовано математичне доведення того, що магічні гексагони за певним правилом побудови існують для будь-якого n (n = довжина сторони шестикутника в сотах).

Загальний час обчислень ШІ становив майже 9 годин. З них система майже 99,9 % часу працювала автономно й не потребувала вводу. Обсяг файлів доведення становив 173 МБ! Формалізація в Lean разом із бібліотеками зайняла майже 8 ГБ місця на диску – у проміжних кроках! Усе доведення розтяглося на 5 днів. Його переривали через ліміти використання тощо.

Незабаром доведення буде опубліковано тут. Чи воно правильне, мають оцінити компетентні люди, які розуміються на математиці краще за автора, що користувався ШІ 😉

Висновок: революція в перевірюваності

ШІ не довів останню теорему Ферма заново, а повністю формалізував у Lean доведення Вайлса, за даними Anthropic, за 11 днів із кількома десятками паралельних агентів. Успіх ґрунтується на двох речах: організації, що тримає стан проєкту видимим, і асистенті доведення Lean, який приймає лише те, що випливає.

Розвиток з 2024 року показує, що ШІ дедалі частіше видає математичні докази. Скільки з цього нове, а скільки відомий матеріал, треба оцінювати щоразу окремо, до цього закликає й вікі Тао. Там, де задіяний Lean, коректність лишається перевірюваною. У цьому й полягає справжній прогрес: не більше тверджень, а машинно підтверджена певність.