Відчувається, що штучний інтелект майже щотижня вирішує нову математичну задачу. У минулому місяці лише OpenAI опублікувала 719 рукописів, у яких стверджувалося, що вирішено деякі найскладніші проблеми галузі. Навіть перевірка комп’ютером може бути помилковою. Після років наповнення штучним інтелектом, люди не можуть не запитати: чи стане математика наступною галуззю, яка постраждає?
AxiomMath може уникнути такої долі, не сповільнюючи темпи, а будуючи більш міцну основу. Ця стартап-компанія з оцінкою 1,6 мільярда доларів США прагне створити перевірений базовий рівень, на який зможуть покладатися AI-агенти для написання програмного забезпечення та, в кінцевому підсумку, проведення наукових досліджень.
У середу компанія оголосила, що офіційно підтвердила проект Stacks — один із найбільших математичних досягнень, написаних людьми. Математики зазвичай високо цінують Stacks. Математик з Колумбійського університету Петер Войт назвав його «майже немає нічого, що могло б з ним порівнятися», і порівняв цей проект із «відомою серією Bourbaki» — серією творів, які у XX столітті перебудували математику з основ.
Колега Войта з Колумбії Йохан де Йонг запустив проект Stacks у 2005 році як відкритий посібник. З тих пір математики постійно вносять до нього внесок, розширюючи його від університетської алгебри до найсучасніших ідей в галузях алгебри, геометрії та теорії чисел.
Група AI-агентів компанії переклала цю базу даних зі 7 654 сторінок у приблизно 16 мільйонів рядків коду, який можна перевірити за допомогою комп’ютера.
Метою формалізації математики є забезпечення надійності її базової структури. Математики переписують доведення у вигляді коду за допомогою мови програмування під назвою Lean, а потім програма-асистент доведень перевіряє цей код рядок за рядком. Якщо доведення проходить перевірку, математики можуть бути впевнені, що воно логічно обґрунтоване.
Інженери також використовують той самий підхід — формальну верифікацію — для перевірки, чи є проект чіпа реалізованим; французькі дослідники використали його для виявлення вразливості в програмному забезпеченні розрахунку сімейних допомог.
Для таких проектів, як Stacks Project, перевірка теорем по одній — це лише частина роботи. Теореми та визначення в Stacks взаємопов’язані, і кожна з них базується на попередніх. Як родовід, багато результатів у Stacks можна прослідкувати до раніших результатів.
Ця взаємозалежність спочатку не дозволяла Axiom впевнено стверджувати, чи є цей проект здійсненним. Команді довелося підтримувати цілісність усіх зв’язків у приблизно 16 мільйонах рядків коду Lean.
Генеральний директор Axiom Каріна Хонг сказала TechCrunch: «У реальності величина та точність зазвичай несумісні. [Stacks] — це сукупність математичних результатів, що становлять математичну основу. Ви хочете, щоб [теореми] були взаємно сумісними, а не суперечили одна одній, як парадокси. Ви також хочете, щоб ці визначення не суперечили одне одному.»
Цей 25-річний генеральний директор кинув докторську програму з математики у Стенфордському університеті та заснував цю компанію у березні 2025 року. У березні цього року Axiom здобула 200 мільйонів доларів США у серії A, яку очолив Menlo Ventures.
Хон сказав: «Ми тоді не були впевнені, чи зможе vibe coding зберегти красу Stacks».
Щоб завершити цей проект, команда надала агентам гнучку структуру та запустила їх паралельно. Ашвін Свамінатхан, член технічної команди Axiom, сказав: «Щодо Stacks ми встановили ієрархію… але не таку, яка точно визначає, що має робити кожен агент. Агенти самі знаходять завдання та визначають, що можна обробляти паралельно».
Axiom також навчила свої моделі вирішувати математичні задачі. Хонг сказав, що цей підхід не використовують більшість інших стартапів у сфері верифікації. Спочатку команда залежала від внутрішнього експерта з Lean, який навчав агентів формувати схожі на людські критерії оцінки. З часом, за словами Хонга, агенти навчилися цій здатності самостійно.
Цей досягнення заповнило одну з найбільших прогалин у формальній математиці. «Коли ви дивитеся на вже формалізовані математичні матеріали, ви бачите величезну чорну діру. І ця чорна діра охоплює алгебраїчну геометрію», — сказав Свамінатан.
Свамінатхан сказав, що до цього дослідники, які хотіли використовувати Lean для перевірки нових робіт з алгебраїчної геометрії, майже не мали готової бази. «Зараз вони її мають.»
Axiom вважає, що кожен перевірений результат стає будівельним блоком, на якому майбутні доведення можуть базуватися на вже перевіреній математиці, не починаючи з нуля. Математик з UCLA, лауреат Філдсівської премії Теренс Тао скоротив це до більш стислої формулювання: «Чим більше у вас формалізованих доведень, тим більше ви зможете зробити формалізованих доведень».
Цільова аудиторія Axiom — не лише математики. Розробники вже довгий час прагнуть забезпечити відсутність вразливостей і безпеки у своєму коді. Зі зростанням кількості програмного забезпечення, що пишуть AI-агенти, ця проблема стане лише гострішою.
Axiom ставки: майбутнє програмне забезпечення має ґрунтуватися на перевірених основах, як сьогодні Stacks.
Свамінатан сказав: «Ми вважаємо, що математика — це галузь, з якої ви починаєте будувати ці речі, і це переносима навичка. Агенти можуть читати наш код, розуміти його та будувати на ньому нову інфраструктуру. Формалізації, які ми зробили за допомогою Lean, зараз є фундаментом, на якому агенти можуть будувати».
Спосіб, яким Axiom створює агентів для Stacks — паралельна робота та вибір завдань самостійно — саме такий, якого Hong очікує в майбутньому для багатьох AI-завдань. Вона вважає, що AI-агентам потрібна добре структурована та повторно використовувана база знань, щоб уникати генерації сміття.
Хонг сказав: «Ви хочете, щоб [агент] мав повторно використовувану базу, на якій вони могли б продовжувати будувати і постійно розширювати межі. Якщо на початку заповнити її поганими інженерними рішеннями, то їм буде важко розширити ці межі».
Хонг дуже впевнена у цьому підході і навіть публічно викликає на виклик. Вона каже: «Я публічно викликаю всі програмні компанії зробити такий масштаб формалізації».