Групоїд Інфініті

Лабораторія «Групоїд Інфініті» <a href="https://groupoid.space/institute/index.htm">Інституту формальної математики</a> займається дослідженням та розробкою інструментів для формальної математики, створенням мов програмування для математичних доведень та аналізу, а також верифікацією теорем за допомогою сучасних обчислювальних методів.

Про лабораторію

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

Процес роботи

Робота лабораторії базується на головному артефакті — методології верифікації теорем <a href="https://axio.groupoid.space">AXIO/1</a> та системі мов AXIOSIS. Ця система дозволяє механізувати будь-яку математичну теорему кількома способами:

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

Місія

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

Принципи роботи лабораторії

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

Наукові напрямки

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

Розроблені мови програмування

• <a href="https://laurent.groupoid.space">Laurnt Schwartz</a> — теорія типів для функціонального аналізу.
• Ernst Zermelo — теорія типів для ZFC із законом виключеного третього.
• Paul Cohen — теорія типів для кардинальних систем із великими кардиналами та форсингом.
• <a href="https://henk.groupoid.space">Henk Barendregt</a> — теорія типів для чистого залежного лямбда-числення.
• <a href="https://per.groupoid.space">Per Martin-Löf</a> — теорія типів для фібраційного підходу та індуктивних типів.
• <a href="https://anders.groupoid.space">Anders Mörtberg</a> — теорія типів для кубічного CCHM/CHM/HTS варіанту.
• <a href="https://dan.groupoid.space">Dan Kan</a> — сімпліціальна гомотопічна теорія типів (Kan, Rezk, Saegal режими).
• <a href="https://fabien.groupoid.space">Fabien Morel</a> — теорія типів для A¹-гомотопічної теорії.
• <a href="https://jack.groupoid.space">Jack Morava</a> — теорія типів для хроматичної гомотопічної теорії та K-теорії.
• <a href="https://urs.groupoid.space">Urs Schreiber</a> — теорія типів для еквіваріантної супергеометрії.

Стан проєкту

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

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

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

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