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