Лабораторія «Групоїд Інфініті» Інституту формальної математики займається дослідженням та розробкою інструментів для формальної математики, створенням мов програмування для математичних доведень та аналізу, а також верифікацією теорем за допомогою сучасних обчислювальних методів.
Лабораторія обчислювальної математики «Групоїд Інфініті» курує розробку та дослідження мов програмування для математиків.
Робота лабораторії базується на головному артефакті — методології верифікації теорем AXIO/1 та системі мов AXIOSIS. Ця система дозволяє механізувати будь-яку математичну теорему кількома способами:
- Безпосереднім вбудовуванням примітивів теорії у верифікатор (для найефективніших обчислень).
- Обчисленням примітивів в іншій теорії (для дослідження виводимості в примітивних базисах).
Надання всій математиці потужної обчислювальної семантики.
- Експліцитна типізація — чітке визначення типів для швидкості, надійності та прозорості.
- Мінімальні ядра — дослідження компактних і ефективних базових конструкцій.
- Підтримка сильних властивостей — гарантія математичної коректності та строгих інваріантів.
- Фокус на швидкості тайпчекінгу — оптимізація процесу перевірки типів для практичної застосовності.
- Педагогічність і лаконічність — створення зрозумілих інструментів для навчання й досліджень.
- Модульність і композиційність — розробка розширюваних та комбінованих систем.
- Формальна верифікація — доведення коректності програм і математичних конструкцій.
- Універсальність абстракцій — створення гнучких інструментів для широкого спектра математичних задач.
- Диференціальна геометрія
- Алгебраїчна топологія
- Супергеометрія
- Стабільна хроматична теорія гомотопій
- Сімпліціальна геометрія
- K-теорія з точки зору теорії типів
- Julius Dedekind — теорія типів для дійсних чисел.
- 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 рік інтегровані у систему, що дозволяє працювати з ними в єдиній обчислювальній парадигмі.