Команда под руководством профессора Сюй Дишэна из Университета Большого залива и Шанхайской лаборатории искусственного интеллекта доказала гипотезу Гиса в комплексной размерности три (комплексный аналог трехмерного пространства). Эта задача оставалась открытой более 30 лет. Результат получен в ходе многократного взаимодействия математиков с ИИ-моделью Intern-S2 и последующей формальной проверки в Lean. Об этом сообщает Шанхайская лаборатория искусственного интеллекта.

Гипотезу предложил в 1995 году французский математик Этьен Гис. Она касается голоморфных систем Аносова — динамических систем, которые одновременно растягивают пространство в одних направлениях и сжимают в других, порождая хаотическое поведение. Гипотеза предсказывает, что само существование такой динамики накладывает жесткие ограничения на геометрию пространства.

В новой работе доказан случай коразмерности один, который, как отмечают авторы, включает и комплексную размерность три (в размерности три разбиение Аносова всегда дает набор комплексных размерностей 2 и 1, то есть одно из направлений заведомо имеет коразмерность один. — Прим. ред.). В случае коразмерности один пространство обязано быть комплексным тором, а динамика с помощью голоморфной замены координат сводится к гиперболическому автоморфизму тора. Это закрывает гипотезу в комплексной размерности три. В более высоких размерностях она в общем случае остается открытой.

Автор математической статьи — Цзесун Чжан из Королевского технологического института (Швеция), ученик и соавтор Сюй Дишэна. Сюй ранее изучал трехмерный случай вместе со своим научным руководителем, лауреатом Филдсовской премии Артуром Авилой, но успешной стратегии доказательства тогда найти не удалось.

Сотрудничество с лабораторией началось в 2026 году. Модель Intern-S2 — мультимодальная система, сочетающая широкую научную предподготовку со специализированным обучением на исследовательской математике. С августа она исследовала гипотезу в нескольких направлениях: первый раунд дал отчет примерно на 400 страниц с возможными аргументами и выкладками. Математики оценивали материал, отсекали непродуктивные подходы и задавали направление следующего раунда. Всего прошло семь раундов: граф задач вырос с 15 до 389 узлов, а объем рабочих материалов достиг примерно тысячи страниц. Итоговое доказательство стало результатом этой итеративной работы — в декларации об использовании ИИ Чжан указывает, что применял внутреннюю версию Intern-S2 для развития идей и аргументов, самостоятельно проверил все выкладки и несет полную ответственность за рукопись.

Отдельный этап — формальная верификация. Команда Пекинского университета под руководством профессоров Биня Дуна и Жочуаня Лю перевела четыре главные теоремы статьи в Lean с помощью собственного фреймворка SHEAF. Процесс занял около пяти дней, в нем одновременно участвовали до 100 агентов, объем кода составил примерно 550 тысяч строк. SHEAF организовал определения, формулировки и зависимости доказательств в направленный ациклический граф, что позволило вести взаимосвязанные задачи параллельно. Специалисты отдельно проверили, что итоговые формальные утверждения соответствуют теоремам в статье, а Lean проверил сами доказательства при заявленных допущениях.

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

Изображения: Magnific (в шапке); Шанхайская лаборатория искусственного интеллекта

Подписывайтесь на каналы Let AI be в Telegram и «ВКонтакте» — оставайтесь в курсе главных новостей в сфере искусственного интеллекта!