Ми — українська open-source лабораторія, що спеціалізується на формалізації математики через гомотопічну теорію типів (HoTT), залежні типи та механічно верифіковані системи доведення теорем. Проєкти реалізовано переважно на OCaml та Agda, з фокусом на уніфікацію синтетичної та класичної математики в єдиному верифікованому фреймворку AXIO/1. Ми розвиваємо спеціалізовані внутрішні мови (Anders, Dan, Jack, Urs, Fabien та інші), що охоплюють ∞-категорії, стабільні спектри, когезивні модальності, реальні числа, ZFC, великі кардинали, форсинг, супergeометрію та еквіваріантну теорію.

Фібраційні істотні істинні сутності лабораторії:

• alonzo — Мінімальна внутрішня мова декартово-замкнених категорій
• yves — Мінімальна внутрішння мова симетричних моноїдальних категорій
• henk — Чиста система з всесвітами
• frank — Мінімальна індуктивна система
• christine — Автоматизована система доведення теорем на основі числення індуктивних конструкцій
• laurent — Теорія типів для теорем математичного і функціонального аналізів
• per — Система доведення теорем на основі W-індукції
• anders — Модальний гомотопічний верифікатор математики
• dan — Сімпліціальна теорія типів
• urs — Еквіваріантна теорія типів супергеометрії
• fabien — A¹ Теорія гомотопій
• jack — Теорія типів Джека Морави

Спеціалізовані мови:

• joe — Компілятор і віртуальна машина Erlang/OTP
• eijiro — Компілятор і віртуальна машина MinCaml
• leslie — Верифікатор розподілених у просторі і часі протоколів TLA+

Наша мета — досягти грандіозного синтезу синтетичної та класичної математики в механічно верифікованому середовищі, об’єднавши алгебраїчні, аналітичні, геометричні, категорійні, топологічні та фундаментальні розділи в єдиній системі залежних типів. Ми прагнемо створити відкриту екосистему proof assistants та внутрішніх мов, доступну для дослідників, математиків та розробників, з акцентом на формальну коректність, кубічні/сімпліціальні HoTT, A¹-гомотопії та супergeометрію. Віримо, що ∞-групоїди та залежні типи — ключ до красивої та єдиної формальної математики майбутнього, а механічна верифікація має стати стандартом для всіх математичних теорем.

• Коректність — усі системи базуються на залежних типах, з повною механічною перевіркою.
• Відкритість — весь код open-source під permissive-ліцензіями.
• Мінімалізм — внутрішні мови та системи мінімальні, але виразні, з фокусом на математичну чистоту.
• Уніфікація — синтез класичних (ZFC, аналіз) та синтетичних (HoTT, ∞-категорії) підходів у єдиному фреймворку.
• Модульність — окремі мови можуть використовуватися незалежно або як частини великої системи AXIO.
• Академічність — підтримка воркшопів, презентацій та освітніх матеріалів для поширення формальних методів.

🇺🇦 Зроблено в Україні з фокусом на гомотопічну теорію типів та формальну математику.

Groupoid Infinity є частиною досліджень Synrc Research Center, присвячених формальним мовам, залежним типам та механічній верифікації математики. Лабораторія підтримує освітні ініціативи, воркшопи та публікацію матеріалів з HoTT і сучасної категорійної математики.

˙

˙

Монографія — Інститут — Бібліотека

Copyright © 2016—2026 Максим Сохацький