Ми — українська open-source лабораторія, що спеціалізується на формалізації математики через гомотопічну теорію типів (HoTT), залежні типи та механічно верифіковані системи доведення теорем. Проєкти реалізовано переважно на OCaml та Agda, з фокусом на уніфікацію синтетичної та класичної математики в єдиному верифікованому фреймворку AXIO/1. Ми розвиваємо спеціалізовані внутрішні мови (Anders, Dan, Jack, Urs, Fabien та інші), що охоплюють ∞-категорії, стабільні спектри, когезивні модальності, реальні числа, ZFC, великі кардинали, форсинг, супergeометрію та еквіваріантну теорію.
Наша мета — досягти грандіозного синтезу синтетичної та класичної математики в механічно верифікованому середовищі, об’єднавши алгебраїчні, аналітичні, геометричні, категорійні, топологічні та фундаментальні розділи в єдиній системі залежних типів. Ми прагнемо створити відкриту екосистему proof assistants та внутрішніх мов, доступну для дослідників, математиків та розробників, з акцентом на формальну коректність, кубічні/сімпліціальні HoTT, A¹-гомотопії та супergeометрію. Віримо, що ∞-групоїди та залежні типи — ключ до красивої та єдиної формальної математики майбутнього, а механічна верифікація має стати стандартом для всіх математичних теорем.
- Коректність — усі системи базуються на залежних типах, з повною механічною перевіркою.
- Відкритість — весь код open-source під permissive-ліцензіями.
- Мінімалізм — внутрішні мови та системи мінімальні, але виразні, з фокусом на математичну чистоту.
- Уніфікація — синтез класичних (ZFC, аналіз) та синтетичних (HoTT, ∞-категорії) підходів у єдиному фреймворку.
- Модульність — окремі мови можуть використовуватися незалежно або як частини великої системи AXIO.
- Академічність — підтримка воркшопів, презентацій та освітніх матеріалів для поширення формальних методів.
Артефакти лабораторії:
- yves — Мінімальна внутрішння мова симетричних моноїдальних категорій
- joe — Мінімальна внутрішня мова декартово-замкнених категорій
- alonzo — Типізоване -גчислення
- leslie — Верифікатор розподілених у просторі і часі протоколів TLA+
- henk — Чиста система з всесвітами
- frank — Мінімальна індуктивна система
- per — Система доведення теорем на основі W-індукції
- christine — Автоматизована система доведення теорем на основі числення індуктивних конструкцій
- anders — Модальний гомотопічний верифікатор математики
- urs — Система доведення теорем на основі W-індукції
- laurent — Теорія типів для теорем математичного і функціонального аналізів
- jack — Теорія типів Джека Морави
- dan — Сімпліціальна теорія типів
- fabien — A¹ Теорія гомотопій
🇺🇦 Зроблено в Україні з фокусом на гомотопічну теорію типів та формальну математику.
Groupoid Infinity є частиною досліджень Synrc Research Center, присвячених формальним мовам, залежним типам та механічній верифікації математики. Лабораторія підтримує освітні ініціативи, воркшопи та публікацію матеріалів з HoTT і сучасної категорійної математики.
˙
˙
Монографія — Інститут — Бібліотека
Copyright © 2016—2026 Максим Сохацький
