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

Лабораторія обчислювальної математики «Групоїд Інфініті» курує розробку та дослідження мов програмування для математиків.

Робота лабораторії базується на головному артефакті — методології верифікації теорем AXIO/1 та системі мов AXIOSIS. Ця система дозволяє механізувати будь-яку математичну теорему кількома способами:

• Безпосереднім вбудовуванням примітивів теорії у верифікатор (для найефективніших обчислень).
• Обчисленням примітивів в іншій теорії (для дослідження виводимості в примітивних базисах).

Надання всій математиці потужної обчислювальної семантики.

• Експліцитна типізація — чітке визначення типів для швидкості, надійності та прозорості.
• Мінімальні ядра — дослідження компактних і ефективних базових конструкцій.
• Підтримка сильних властивостей — гарантія математичної коректності та строгих інваріантів.
• Фокус на швидкості тайпчекінгу — оптимізація процесу перевірки типів для практичної застосовності.
• Педагогічність і лаконічність — створення зрозумілих інструментів для навчання й досліджень.
• Модульність і композиційність — розробка розширюваних та комбінованих систем.
• Формальна верифікація — доведення коректності програм і математичних конструкцій.
• Мінімалізація залежностей — краще повна їх відсутність.
• Універсальність абстракцій — створення гнучких інструментів для широкого спектра математичних задач.

• Диференціальна геометрія
• Алгебраїчна топологія
• Супергеометрія
• Стабільна хроматична теорія гомотопій
• Сімпліціальна геометрія
• K-теорія з точки зору теорії типів

• Laurnt Schwartz — теорія типів для функціонального аналізу.
• Ernst Zermelo — теорія типів для ZFC із законом виключеного третього.
• Paul Cohen — теорія типів для кардинальних систем із великими кардиналами та форсингом.
• Henk Barendregt — теорія типів для чистого залежного лямбда-числення.
• Per Martin-Löf — теорія типів для фібраційного підходу та індуктивних типів.
• Anders Mörtberg — теорія типів для кубічного CCHM/CHM/HTS варіанту.
• Dan Kan — сімпліціальна гомотопічна теорія типів (Kan, Rezk, Saegal режими).
• Fabien Morel — теорія типів для A¹-гомотопічної теорії.
• Jack Morava — теорія типів для хроматичної гомотопічної теорії та K-теорії.
• Urs Schreiber — теорія типів для еквіваріантної супергеометрії.

Система досягає синтезу синтетичної та класичної математики. Її типи охоплюють:

• Симпліціальні ∞-категорії
• Стабільні спектри
• Модальності
• Дійсні числа
• ZFC
• Великі кардинали
• Форсинг

Усі відомі математичні області станом на 2025 рік інтегровані у систему, що дозволяє працювати з ними в єдиній обчислювальній парадигмі. Для освітніх цілей створено систему мов AXIOSIS для платформи Ericsson Erlang/OTP.

Максим Сохацький, старший науковий співробітник НТУУ "КПІ" ім. Ігоря Сікорського, 2025, Київ.