Шестимерная сфера: формальное доказательство существования комплексной структуры

Formalization of the Solution to the Hopf Problem

Репозиторий HopfProblem на GitHub содержит формализацию на языке Lean решения проблемы Хопфа: шестимерная сфера допускает структуру комплексного многообразия, совместимую со стандартной топологией. Формализация основана на работе Леванта Альпёге «A compact complex threefold fibred by tori over the projective line, and the six-sphere» и включает настройку Comparator для проверки утверждения. Код можно проверить онлайн.