Математическая свалка Сепы

2006 год.
Масуда и Панов задаются вопросом о том, верно ли, что квазиторическое многообразие однозначно определяется своим целочисленным кольцом когомологий.

https://arxiv.org/pdf/math/0607094v1

Этот вопрос становится известным как вопрос о когомологической жёсткости для (квази)торических многообразий.

2022 год.
Я начинаю работать в BIMSA и знакомлюсь с Син Фу, которая работает в области торической топологии. Мы с ней дружим, даже пишем какую-то статью вместе (пример орграфа с разными путевыми эйлеровыми характеристиками над разными полями). В 2025 году она переезжает работать в Шанхай, в SIMIS.

3 сентября 2026 года.
Выходит GPT-6 Astra.

8 сентября.
OpenAI заявляет о решении проблемы Навье–Стокса.

7–11 сентября.
Проходит конференция PPICTA в Осаке, на которой я встречаю Син. Она рассказывает мне, что сейчас работает над положительным решением частного случая задачи о когомологической жёсткости (квази)торических многообразий. Мы начинаем обсуждать эту задачу и оба соглашаемся, что в общем случае должен быть контрпример. Я говорю, что его можно построить при помощи ИИ. Она не соглашается со мной. Я воспринимаю это как вызов.

Известно, что контрпримеров нет, если вещественная размерность многообразия меньше 6. Дальше в течение пары недель я сливаю лимиты ChatGPT, оставшиеся в конце недели, на поиск контрпримера в размерности 6. Моя единственная мотивация — доказать Син, что ИИ может находить такие контрпримеры. Но он не находит.

28 сентября.
Я прошу его построить контрпример в любой размерности, необязательно в размерности 6. И он за пару часов находит контрпример в размерности 8.

В процессе использует данные, которые сохранил для себя про размерность 6: получившиеся контрпримеры — это проективные расслоения над торическим многообразием размерности 6.

Ещё раз подчеркну, что я ни разу не специалист в торической топологии, я попросил чатик построить этот контрпример, только чтобы переубедить Син.

Я рассказываю Син о решении. Жалею, что не поспорил с ней на деньги. Через пару часов я прошу её пока никому не рассказывать об этом решении. К этому моменту она уже рассказала одному своему соавтору. Он рассказывает ещё нескольким коллегам.

29 сентября.
Информация доходит до Стивена Тиро (Stephen Theriault). Он пишет нам письмо о том, что в тот же день (опять!) ему прислали информацию о том, что два других автора — Tao Gong и Yingxin Li — тоже построили такой пример. Их примеры слегка отличались от наших. Мы пишем им письмо, предлагая созвониться. Они сразу соглашаются. В тот же день мы созваниваемся. Они говорят, что построили свой пример уже некоторое время назад и у них уже есть оформленная статья. Мы решаем, что, раз у них уже есть написанная статья, они должны немедля выложить её в архив, что они и делают.

https://arxiv.org/pdf/2609.39707v1

Договариваемся работать дальше над этой темой вместе и позже выложить новую версию статьи с четырьмя авторами.

Дальше мы начинаем созваниваться и работать вместе. Для меня было важно чётко указать гомотопический инвариант, который отличает эти примеры с изоморфными кольцами когомологий. И через пару дней мы его нашли. Это некоторое подмножество в произведении групп когомологий:

SZ^{n,m}(X) ⊆ H^n(X) × H^m(X).

Точнее говоря, нужно рассматривать кольцо когомологий вместе с этими подмножествами, как дополнительной структурой.

Мы сильно обобщили конструкцию. Теперь она начинается с любого 6-мерного многообразия с некоторыми свойствами, и мы смотрим на некоторые проективные расслоения над ним, и выписываем условия, при которых они получаются не гомотопически эквивалентными, но имеющими изоморфные кольца когомологий. По пути мы ещё доказали, что пятикратные надстройки получившихся примеров гомотопически эквивалентны.

7 ноября.
Послали новую версию статьи в архив. Вот только что появилась онлайн:

https://arxiv.org/abs/2609.39707

Axiom Math выпустила Lean-версию Stacks Project

4 ноября Axiom Math опубликовала созданную с помощью ИИ формализацию Stacks Project — открытого справочника по алгебраической геометрии объёмом около 7500 страниц. Проект начал математик Йохан де Йонг в 2005 году, и с тех пор его развивали сотни авторов. По данным Axiom Math, версия на Lean насчитывает около 16 млн строк кода.

Определения и теоремы из библиотеки можно подключать к новым доказательствам. На сайте проекта можно открыть рядом исходную формулировку и её версию на Lean, а также посмотреть, от каких результатов она зависит.

Код разделён на две части. В StacksCore собраны формализации, которые специалисты уже сверили с оригиналом. В StacksFrontier находится код, написанный ИИ-агентами: по данным разработчиков, доказательства проходят проверку Lean, а соответствие формулировок исходному тексту ещё предстоит проверить людям. Некоторые примеры, упражнения и замечания пока не формализованы.

Анонс команды:
https://axiommath.ai/research/the-stacks-project-formalized/

Сайт проекта:
https://stacks.axiommath.ai/

Открытый репозиторий:
https://github.com/AxiomMath/Stacks