В Китае с помощью ИИ доказали математическую гипотезу Гиса, открытую в 1995 году
Китайские математики с помощью научной модели искусственного интеллекта Intern-S2 доказали трехмерный случай гипотезы Гиса — задачи из области комплексной динамики, которую французский математик Этьен Гис сформулировал в 1995 году. Результат описан в препринте на arXiv, а основные теоремы проверила команда Пекинского университета с помощью системы Lean. Об этом сообщила Шанхайская лаборатория искусственного интеллекта.
Что за гипотеза
Гипотеза Гиса касается особых математических систем, в которых движение развивается по сложным, но строго определенным правилам. Такие системы называют голоморфными системами Аносова. Они описывают динамику в комплексных пространствах — математических объектах, которые обобщают привычные геометрические пространства с помощью комплексных чисел.
Гис предположил, что подобные системы можно представить в более упорядоченном виде — как преобразования определенных пространств с жесткой геометрической структурой. Если гипотеза верна, то за сложным движением можно обнаружить простую математическую основу.
Новая работа доказывает это для систем коразмерности один, включая случай комплексной размерности три. Более общий вариант гипотезы пока остается открытым.
Как помог искусственный интеллект
Работой руководил Сюй Дишэн, профессор Университета Большого залива и приглашенный исследователь Шанхайской лаборатории ИИ. Ключевую роль сыграл также математик Цзеcун Чжан из Королевского технологического института в Стокгольме. При этом в опубликованном препринте Чжан указан единственным автором, а Сюй упомянут в благодарностях за научные обсуждения.
С августа 2026 года команда использовала Intern-S2 для поиска доказательства. Уже на первом этапе модель подготовила около 400 страниц выкладок. После семи циклов работы объем рассуждений превысил тысячу страниц, а число узлов в схеме решения выросло с 15 до 389.
Модель перебирала математические подходы и развивала длинные цепочки рассуждений. Ученые оценивали результаты, выбирали перспективные идеи и задавали направление дальнейшей работы. Таким образом, доказательство стало результатом совместной работы людей и ИИ, а не самостоятельного решения задачи моделью.
Проверка с помощью компьютера
Чтобы проверить строгость доказательства, команда Пекинского университета использовала Lean — систему, которая позволяет формально записывать математические утверждения и автоматически проверять логические шаги. Для работы применили SHEAF, разработанную исследователями систему с ИИ-агентами.
По данным Шанхайской лаборатории, проверка заняла около пяти дней. Команда подготовила примерно 550 тысяч строк кода Lean, а несколько агентов работали параллельно. Код проверки опубликовали в открытом доступе на GitHub.
Препринт еще не прошел рецензирование в научном журнале. Поэтому результат пока следует рассматривать как опубликованное математическое доказательство, прошедшее формальную машинную проверку, но не как окончательное решение всей гипотезы Гиса.
