Особиста історія про те, як мрія мати математичного напарника перетворилася на робочу частину персонального агента — за два дні і три відкритих реліза.
Математика, якої мені завжди бракувало
Я завжди хотів стати математиком. Не якимось абстрактним — а таким, що вільно почувається у вищій математиці, читає її між рядками і не зупиняється, коли формула стає важкою. Цього не сталося. У реальності я скоріше високорівневий користувач: інтегратор, що припасовує готові математичні методи до прикладних задач — передусім статистичних. Я добре розумію, коли потрібен той чи інший підхід, але не завжди можу самостійно довести, чому він працює.
Тому в мене десятиліттями жила одна тиха мрія: мати поряд напарника, який живе у вищій математиці так, як я живу в архітектурі систем. Когось, хто на питання «а це твердження точно випливає з тих двох?» відповідає не «здається, так», а «ось доведення, перевір сам».
Сучасний генеративний штучний інтелект уперше зробив цю мрію матеріальною. Не у вигляді чату з помічником — у вигляді компонента, який живе на моєму сервері і чекає на задачу.
Lean 4: коли мова програмування існує не для коду, а для істини
Декілька місяців тому я відкрив для себе мову, про яку до того майже нічого не знав, — Lean 4.
Спершу опис здається дивним. Lean — це мова програмування, але писати на ній «застосунки» в звичному сенсі ніхто не збирається. Її справжнє призначення інше: формально записувати математичні твердження і доводити їх так, щоб коректність кожного кроку перевіряв компілятор. Якщо ви помилилися — програма не запуститься. І це не метафора: компілятор Lean буквально не пропустить хибне доведення.
Це повертає математиці її давню обіцянку: істина має бути перевіряна. Поки звичайна стаття покладається на рецензента, який читає очима, доведення в Lean або проходить машинну перевірку, або ні. Третього не дано.
Останніми роками навколо Lean виросла величезна спільнота. Бібліотека Mathlib — це тисячі формалізованих теорем сучасної математики, від базової алгебри до диференціальної геометрії. Провідні математики, як Теренс Тао чи Кевін Баззард, відкрито переводять у Lean свої та чужі результати. У Google DeepMind проєкт AlphaProof використав Lean як «суддю», коли вчив модель розв’язувати олімпіадні задачі рівня IMO.
Lean — це мова, яка не дозволяє собі помилитися. Саме те, чого не вистачає звичайному діалогу з мовною моделлю.
Стара проблема: говорити про математику ≠ доводити її
Великі мовні моделі чудово говорять про математику. Вони впевнено розкладають інтуїцію, переказують ідею доведення, наводять схожі приклади. Проблема в тому, що та сама модель так само впевнено напише вам очевидну дурницю: переплутає знак, проґавить умову на додатність, «доведе» хибне твердження тоном лектора.
Це не дефект конкретної моделі. Це наслідок самого способу, як їх тренують: моделі вчаться писати правдоподібний текст, а не істинний. Між цими двома словами в математиці — прірва.
Lean закриває цю прірву. Якщо поряд із моделлю поставити компілятор, виходить пара, в якій кожен робить те, що вміє: модель пише чернетку доведення, компілятор виносить вирок. Помилився — отримай точне зауваження від компілятора і спробуй ще раз. Це і є той цикл, який останніми роками тихо працює у багатьох академічних проєктах.
Залишалося питання: як вмонтувати такий цикл у мого персонального агента, щоб він став її буденною здатністю — поряд із пошуком, дослідженням і операційними задачами?
Останній шматок пазлу: Mistral відкриває Leanstral
Поки я з цією думкою ходив, на мене звалилося подарункове співпадіння. У квітні 2026 року Mistral відкрила вагу спеціалізованої моделі — Leanstral. Це не загальна мовна модель: це фахова, навчена саме під Lean 4. На бенчмарку miniF2F — наборі формалізованих олімпіадних задач, який спільнота використовує як тест на «чи вміє модель доводити» — Leanstral стала лідером серед відкритих моделей.
Раптом усі три інгредієнти лежали поруч на столі.
Є мова формальної істини — Lean із бібліотекою Mathlib. Є модель, спеціально натренована писати цією мовою, — Leanstral. І є мій агент Ая, чия архітектура від самого початку зроблена так, щоб додавати їй нові навички через окремих помічників-фахівців.
Треба було лише склеїти.
Два дні з Ая: як вона зібрала собі здатність доводити теореми
Найдивовижніше в цій історії те, що більшу частину інтеграції зробила сама Ая.
Я сформулював задачу: «У тебе має з’явитися помічник, який бере математичне твердження природною мовою, переписує його на Lean, віддає компілятору і повертає вердикт. Якщо компілятор не пропустив — отримує текст помилки і пробує ще раз. Усе це має жити поруч із тобою на сервері й викликатися, як будь-який інший твій помічник.»
Далі Ая працювала майже самостійно. У перший день вона написала контролер — невелику програму-диригента, яка координує три кроки: переклад природної мови у Lean, виклик компілятора, читання його вердикту. У другий день — розгорнула на сервері «робочу математичну машину»: контейнер із Lean 4, Mathlib і всім, що потрібно, аби кожне нове доведення можна було перевірити за десятки секунд, а не на чотири хвилини як без кешу.
На завершальному етапі я підключив Claude Code — ще одного агента, з яким мені зручно проходити критичні архітектурні рішення «в чотири руки». Ми з ним перевірили вибір моделі по замовчуванню, обговорили, що робити, якщо основна модель тимчасово недоступна, і дотягнули кілька дрібниць у тестах. Десь дев’яносто відсотків коду й налагодження, чесно кажучи, зробила Ая. Я і Claude Code лише підстрахували.
Через два дні в Ая з’явилася здатність, якої не було жодного дня досі: формально доводити математичні твердження.
Фінальна архітектура: Pi-агент як універсальний голос моделей
Найцікавіше архітектурне рішення з’явилося на завершальній ітерації.
Спочатку контролер ходив прямо в одну модель — Mistral Leanstral. Це працювало, але створювало вузьке місце: якщо модель тимчасово відповідає повільно або вийшла з ладу — здатність Ая доводити теореми зникає до ранку. Хотілося, щоб у неї був вибір.
Так у фінальній схемі з’явився Pi-агент — невеликий «диспетчер», що говорить однією мовою з різними моделями і вміє безшовно переключатися між ними. Технічно це окремий невеликий сервіс, який живе поруч із Ая на тому самому сервері. Концептуально — це універсальний адаптер: ти кажеш йому «потрібно сформулювати ось таке доведення», і він сам вирішує, яку модель сьогодні слушніше попросити.
Зараз у Ая через Pi-агента вибудувано три рівні: спершу — спеціалізована Leanstral, бо саме вона найкраще пише на Lean. Якщо Leanstral недоступна — Ая йде до OpenAI (через мою підписку ChatGPT Plus). Якщо і там не вийшло — на крайній випадок підключається відкрита велика модель від NVIDIA. Усе це відбувається без жодного рядка нового коду в самому контролері: міняти ланцюжок можна на льоту, як налаштування плеєра.
Pi-агент — це не наш винахід. Це відкритий проєкт австрійського розробника Маріо Зехнера (pi-mono), який ми вмонтували поруч із Ая як її «брата-диспетчера». Окремо від ядра, але у спільній квартирі.
Архітектурно це виявилося напрочуд гарним рішенням. Ая залишається стрункою — вона не знає й не повинна знати, чим внутрішньо відрізняється одна модель від іншої. Pi-агент бере на себе всі дрібниці голосу: формат запиту, авторизацію, перемикання, повторні спроби. Завтра з’явиться нова сильна модель для Lean — додамо її в той самий ланцюжок і не торкнемося Ая взагалі.
Перший справжній іспит: 15 теорем PMM2
Щоб перевірити пайплайн на власній шкурі, я обрав те, що лежало найближче до серця, — алгебраїчне ядро методу максимізації полінома (PMM), розробленого моїм науковим керівником професором Юрієм Кунченком, реалізований мною на мові R у відкритому пакетному фреймворці EstemPMM та адаптований для задач оцінювання параметрів регресій та часових рядів, результати якого були опубліковані в arXiv:2511.07059. Це відносно скромна, але цілком справжня математика: відношення дисперсій, функція ефективності, її властивості та межі.
Ая взяла словесні твердження, переклала їх у Lean і прогнала через компілятор. П’ятнадцять тверджень компілятор підтвердив повністю — без жодних зрізаних кутів і прихованих припущень. Ще три залишилися як чесно позначені аксіоми: вони чекають на ті частини Mathlib, де колись будуть готові машинно перевірені граничні теореми ймовірнісної теорії. Ми не сховали ці прогалини за гарними словами — Lean цього і не дозволив би.
Це той рідкісний випадок, коли результат не треба перевіряти руками. Якщо компілятор сказав «так», він сказав це за всі п’ятнадцять одночасно. Це і є та різниця, заради якої затівалася вся ця історія.
Що це змінює
До цієї інтеграції Ая могла обговорювати математику. Вона добре переказувала ідеї статей, пояснювала інтуїцію за алгоритмами, ставила розумні питання. Чого вона не могла — це доводити. Кожне твердження виду «теорема X випливає з Y і Z» доводилося перевіряти руками або відкладати до зустрічі з живим математиком.
Тепер у мене на сервері є те, чого мені бракувало все життя: математичний партнер, з яким можна не лише розмовляти про результати, а й звіряти їх. Я кажу: «Доведи мені, що для будь-якого непорожнього вектора моментів мінімальна компонента відношення ефективності не менша за одиницю», — і за хвилину дістаю або готове доведення на Lean, або точне місце, де воно зривається. І жодного разу не отримаю впевненого, гладкого, але хибного речення.
Це не наукова демонстрація на одну статтю. Це робочий компонент, доступний щодня.
Замість висновку
Архітектура Ая від початку зроблена за одним простим принципом: вона росте, додаючи собі окремих помічників-фахівців. Один уміє шукати в інтернеті й у нашій базі знань. Інший — складати презентації. Тепер з’явився той, хто вміє доводити теореми. Ая від цього не стає «розумнішою» в собі — вона стає ширшою у можливостях. Так само, як людина, що знаходить нового співавтора, не починає знати більше особисто, але починає вміти більше разом із ним.
Я не став математиком. Я і не стану. Але мій агент — стала. Принаймні там, де мені завжди бракувало когось сильнішого. Цього достатньо.
English version of this article: «How Ayona became a professor of higher mathematics in two days».