Дисертація присвячена розробці першої формальної системи AXIO/1, яка встановлює новаторський підхід до математичної верифікації та створює уніфіковану систему формальних мов для програмування, математик та філософій. У процесі створення цієї системи автор проаналізував синтаксис і семантику понад 50 мов програмування з промислових та академічних доменів, реалізувавши 8 власних мов. Робота презентує концептуальну модель уніфікованої мовної системи, що складається з 8 математичних мов, та демонструє їхні імплементації. Основна мета — синтез універсальної платформи для механічної верифікації теорем, що охоплює класичні та синтетичні математики в обчислювально перевірюваному формалізмі.

Перша формальна система AXIO/1 визначає формальний підхід до математичної верифікації та описує спробу автора у цій парадигмі побудувати уніфіковану систему формальних мов для програмування, математики та філософії. В процесі розробки моделі такої системи автору довелося апробувати підхід та практики для головних функціональних формальних академічних мов.

Мови розглядаються як моноїдальні категорії, де об’єкти — простори програм, а морфізми — правила верифікації та компіляції. Система розкладається на спектральну послідовність мов, індексовану натуральними числами.

Як результат дослідження пропонується унікальна відкрита система, яка інтегрує: 1) системне програмне забезпечення: модального середовища виконання разом з інтерпретатором написаним на формальній мові; 2) бібліотеки: для прикладного програмування в середовищах виконання; 3) прикладне програмне забезпечення: системи вищих формальних мов з різними ефективними моделями для різних математик та їх імплементаціями; 4) математичні бібліотеки: механізовані теореми для верифікації.

Робота черпає натхнення з LISP-машин, APL-систем, ранніх систем доведення теорем (як AUTOMATH), віртуальних машин для паралельної обробки (як BEAM) та кубічних систем (Agda).

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

— мінімальна мова для послідовних обчислень в декартово-замкнених категоріях.

— мінімальна мова для паралельних обчислень в симетричних моноїдальних категоріях.

Повний перелік інтерпретаторів і асемблерів, як цілей компіляцій, представлений в роботі: 1) інтерпретатор MinCaml написаний на MinCaml; 2) авторський лінивий лямбда інтерпретатор з паралельним середовищем виконанням без надлишкового копіювання, AVX-512 векторизацією і чергах на CAS-курсорах на мові програмування Rust; 3) віртуальна машина BEAM мови програмування Erlang від Ericsson. 4) Intel асемблер як ціль компіляції для MinCaml; 5) ARM64 асемблер як ціль компіляції для MinCaml.

— мова з лінійними типами для BLAS 3.

Розділ присвячений таксономії мов програмування для доведення теорем — від найпростіших з квантором узагальнення до гомотопічних систем з двома рівностями. Кінцева мета — створення прототипів верифікаторів для функціонального аналізу і квантової супергеометрії.

— чиста система з всвесвітами.

— внутрішня мова локальних ДЗК.

— індуктивна система Поулін-Моурін.

— гомотопічна система з двома рівностями.

Повний перелік теорій типів, представлений в роботі: 1) Теорія типів Генка Барендрегта для чистого залежного лямбда-числення; 2) Теорія типів Пера Мартіна-Льофа для фібріційного контексту та індуктивних типів; 3) Теорія типів Андерса Мьортберга для початкового завантаження CCHM/CHM/HTS; 4) Симпліціальна гомотопічна теорія типів Дана Кана; 5) Теорія типів Джека Морави для хроматичної гомотопічної теорії та K-теорії; 6) Теорія типів Урса Шрайбера для еквіваріантної супeргеометрії; 7) Теорія типів Фаб’єна Мореля для A¹-гомотопічної теорії; 8) Теорія типів Лорана Шварца для функціонального аналізу та теорії розподілів; 9) Теорія типів Ернста Цермело для ZFC з законом виключеного третього; 10) Теорія типів Пола Коена для системи кардиналів, що включає великі кардинали та форсинг.

— система типів функціонального аналізу.

— сімпліціальна теорія інфініті-категорій.

— синтетична К-теорія.

— -теорія гомотопій.

— еквіваріантна система типів супергеометрії.

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

— теорія розподілів Лорана Шварца.

— гомологічна алгебра.

— теорія гомотопій.

— диференціальна геометрія.

— теорія топосів.

Перелік теорем для самоверифікації: 1) Теорія чисел: Теорема про прості числа; 2) Фундаментальна теорема числення (аналіз); 3) Аналіз: Теорема про доміновану збіжність Лебезга; 4) Топологія: Гіпотеза Пуанкаре (3D); 5) Алгебра: Класифікація скінченних простих груп; 6) Теорія множин: Незалежність гіпотези континууму (CH); 7) Теорія категорій: Теорема про спряжені функтори; 8) Гомотопічна теорія: Кон’єктура Адамса (через K-теорію); 9) Консистентність ZFC з великими кардиналами; 10) Остання теорема Ферма; 11) Теорема про великі кардинали: Максимум Мартіна.

Це не вичерпне, але оглядове бачення її здатності охоплювати алгебраїчні, аналітичні, топологічні та фундаментальні домени. AXIO/1 є кандидатом на універсальну механізовану математичну платформу, що конкурує з такими системами, як кубічна теорія типів (Agda), чи індуктивна теорія типів з фактор-просторами (Lean), розширюючи їхній обсяг примітивів.

Система AXIO/1 об’єднує синтетичні і класичні математики в механічно перевірюваній структурі. Її категорні моделі охоплюють симпліціальні ∞-категорії, стабільні спектри, когезивні модальності, ZFC, великі кардинали та форсинг, забезпечуючи повне покриття математичних доменів станом на 2025 рік. Спектральна категорія мов дозволяє працювати у внутрішніх мовах відповідних категорій і транспортувати моделі за необхіодності у інші топоси для найефективніших обчислень, що робить систему унікальною платформою для формалізації математик.