Формализация высшей теории категорий через HoTT

В 2025 году сообщество Unimath объявило о завершении формализации основ (infinity,1)-категорий с использованием гомотопической теории типов (HoTT). Это позволяет проверять сложнейшие топологические доказательства с помощью компьютерных пруверов вроде Coq и Lean.

Проект объединяет топологию, логику и программирование. Новый фундамент математики исключает человеческие ошибки в абстрактных выводах и предоставляет инструменты для автоматического поиска доказательств в алгебраической топологии.