от длинного списка в github.com/openai/math/blob/main/overview.pdf глаза разбегаются, хочется выбрать несколько конкретных результатов оттуда… вот что ответил на такую просьбу сам chatgpt:

(Техническая оговорка самого ChatGPT: результаты получены не этой версией ChatGPT, а другой внутренней моделью.)

1. Десятая проблема Гильберта над ℚ. Утверждается, что не существует алгоритма, который по многочлену с целыми коэффициентами определяет, имеет ли он рациональный корень. Исходная десятая проблема Гильберта для целых чисел давно решена отрицательно; рациональная версия оставалась одной из центральных открытых задач диофантовой геометрии. Пока без Lean-формализации.

2. Шестнадцатая проблема Гильберта — число предельных циклов. Не вся проблема целиком, но знаменитый вопрос: существует ли для каждого d конечная граница H(d) на число предельных циклов плоского полиномиального векторного поля степени d? Каталог утверждает, что да. Общий результат пока не формализован; в Lean проверен только частный случай.

3. «Квази-гипотеза Римана». Для ζ(s) и всех функций Дирихле L(s, χ) утверждается отсутствие нулей в полуплоскости Re s > 7/8. Это, конечно, далеко не RH с критической прямой Re s = 1/2, но качественно гораздо сильнее известных областей без нулей, сужающихся к прямой Re s = 1. Этот результат формализован в Lean.

4. Гипотеза Ходжа для CM-абелевых многообразий. Утверждается рациональная гипотеза Ходжа для всех комплексных абелевых многообразий CM-типа, во всех размерностях и коразмерностях; в том же семействе — результаты для произведений K3-поверхностей. Если всё верно, последствия очень серьёзные: через теоремы Милна отсюда, в частности, получается гипотеза Тейта для всех абелевых многообразий над конечными полями. Это один из самых крупных, но пока не Lean-формализованных пунктов списка.

5. Unique Games Conjecture Хотта. Одна из центральных гипотез теории сложности и аппроксимационных алгоритмов: модель заявляет её положительное решение. Вместе с этим получаются точные пороги NP-трудности для ряда классических задач вроде Max-Cut и Vertex Cover. Основной результат есть в Lean.

6. Хроматическое число плоскости не меньше шести. В задаче Хадвигера—Нельсона надо раскрасить плоскость так, чтобы точки на расстоянии 1 имели разные цвета. До сих пор было известно 5 ≤ χ(ℝ²) ≤ 7; здесь утверждается, что пяти цветов недостаточно, так что остаются только 6 или 7. Причём без каких-либо предположений измеримости цветов. Формализация в Lean есть.

7. Контрпример к гипотезе Капланского о делителях нуля. Построена конечно заданная группа без кручения G, для которой групповая алгебра 𝔽₂[G] всё-таки имеет ненулевые делители нуля. Рядом в каталоге лежит целый пакет других контрпримеров к гипотезам о групповых алгебрах. Основной контрпример формализован.

8. Контрпример к гипотезе Уолла D(2). Уолл спрашивал: если конечный 3-мерный CW-комплекс X имеет «гомологически двумерное» универсальное накрытие и H³(X; M) = 0 для всех локальных систем коэффициентов M, обязан ли X быть гомотопически эквивалентен конечному 2-мерному CW-комплексу? Каталог заявляет отрицательный ответ. Пока без Lean.

9. Дискретное преобразование Фурье быстрее n log n. Заявлен точный алгоритм сложности O(n (log n)^(1−δ)), где δ = 10⁻¹³, то есть впервые пробивается классический рубеж FFT n log n — правда, в модели точной комплексной арифметики с довольно свободными коэффициентами. Пока без Lean.

10. Умножение целых чисел быстрее n log n. Для двух n-битных чисел заявлено O(n (log n)^(1−κ)), где κ = 2⁻¹⁸². Выигрыш совершенно микроскопический, но качественно это пересекает рубеж n log n и опровергает старую гипотезу Шёнхаге—Штрассена об оптимальности этого порядка в обычной многоленточной модели машины Тьюринга. Пока без Lean.

(Существенный дисклеймер: сама OpenAI подчёркивает, что результаты находятся на разных стадиях проверки, а часть
нефомализованных доказательств может содержать ошибки.)