Матчасть: гипотеза Эрдёша и гипотеза якобиана

‌

Гипотеза Эрдёша и Лейденская декларация

20 мая 2026 года OpenAI сообщила, что ее внутренняя модель опровергла гипотезу Эрдёша о единичных расстояниях — задачу дискретной геометрии, поставленную в 1946 году [1]. Вопрос помещается в одну строку: сколько пар среди n точек на плоскости может лежать на расстоянии ровно 1? Эрдёш предполагал, что ненамного больше, чем у квадратной решетки: порядка n^{1 + c/log log n}. Модель предъявила конструкцию, где таких пар больше, чем n в степени, строго превышающей единицу, — предположенная граница неверна.

Проверку организовали образцово. В день анонса на arXiv.org вышла работа девяти математиков — среди них Нога Алон, Тимоти Гауэрс, Дэниел Литт, Мелани Мэтчетт Вуд — «короткая, переработанная, проверенная людьми версия» машинного аргумента [2]. Аннотация прямо фиксирует происхождение идей: аргумент «решающим образом опирается» на идеи, восходящие — «по крайней мере задним числом» — к работам Элленберга — Венкатеша, Голода — Шафаревича и Хаджира — Мэра — Рамакришны. Конструкция собрана из инструментов, уже имевшихся в литературе, — включая теорему Голода — Шафаревича 1964 года — в комбинации, до которой не доходили люди [2, 7]. В тот же день Уилл Савин отдельной работой довел оценку до явной: существуют конфигурации, где пар больше n^1,014 [3]. Дэниел Литт назвал случившееся «первым автономно порожденным ИИ результатом, который интересен мне сам по себе». Гауэрс при этом подчеркивал, что идеи по отдельности уже присутствовали в литературе [7].

Каркас цифр после проверки. Нижняя граница — n^1,014. Верхняя не менялась с 1984 года: порядка n^4/3 (Спенсер, Семереди, Троттер). Всё между 1,014 и 4/3 — открытая территория. Гипотеза опровергнута, задача жива.

Проверка получила и машинное продолжение. Борис Алексеев (OpenAI) опубликовал полную формализацию аргумента на языке Lean, построенную с помощью модели Sol: около 1,2 млн строк кода за три недели. Для масштаба: mathlib, основную библиотеку формализованной математики, сообщество писало девять лет — в ней 2,3 млн строк [8].

О воспроизводимости известно немного. По данным Science News, при повторных запусках модель приходила к решению примерно в половине попыток; статистику неудач и ошибочных «решений» компания не раскрывает [4]. Штрих из разбора Understanding AI: публичная модель GPT-5.5 справляется с той же задачей, если дать ей небольшую подсказку [9]. Там же — две реплики участников проверки. Томас Блум: «Это может быть верно. Это может быть бессмыслица. Кто будет в состоянии это проверять?» Мелани Мэтчетт Вуд: «ИИ станет незаменимым инструментом в математике». Речь идет о разных вещах: в первой реплике — о пропускной способности проверки, во второй — о пользе инструмента.

Реакция сообщества оформилась в документ. 2 июня опубликована Лейденская декларация об искусственном интеллекте и математике — итог воркшопа в Лоренц-центре Лейденского университета; текст готовили 16 математиков [5]. Декларация перечисляет пять рисков: правдоподобные, но недостоверные доказательства, трудноотличимые от корректных; использование опубликованных работ без атрибуции; доступ к платным системам как условие научного результата; обход рецензирования — анонсы в прессе до проверки сообществом; смещение приоритетов к задачам, удобным для автоматизации. Динамика подписей: 1590 — на 5 июня, 3108 — на 22 июля.

Деталь, замыкающая сюжет: Джордан Элленберг — соавтор одной из тех работ, к которым проверявшие возвели идеи машинной конструкции, — декларацию публично поддержал, подчеркнув, что она «никоим образом не направлена против ИИ» [6].

Статус. Декларация — рекомендательный документ, обязательных норм в математике не появилось. Контрпример прошел человеческую проверку; явная оценка в нем принадлежит уже человеку. Задача Эрдёша остается открытой — в новых границах.

1. openai.com/index/model-disproves-discrete-geometry-conjecture/

2. arxiv.org/abs/2605.20695

3. arxiv.org/abs/2605.20579

4. sciencenews.org/article/ai-guardrails-erdos-math-problem

5. leidendeclaration.ai

6. quomodocumque.wordpress.com/2026/06/04/the-leiden-declaration-on-artificial-intelligence-and-mathematics/

7. theconversation.com/an-ai-solution-to-an-80-year-old-problem-has-shocked-mathematicians-283686

8. xenaproject.wordpress.com/2026/07/20/human-mathematicians-are-being-outcounterexampled/

9. understandingai.org/p/openais-milestone-math-breakthrough

Гипотеза якобиана: контрпример

20 июля 2026 года математик Левент Альпёге (Levent Alpöge, аффилиации — Гарвард и Anthropic) опубликовал в соцсети X три многочлена от трех переменных и сообщил, что это контрпример к гипотезе якобиана — задаче, открытой с 1939 года [10]. По словам Альпёге, отображение построила языковая модель Claude Fable 5.

Гипотеза якобиана (Келлер, 1939) — о полиномиальных отображениях F: Cⁿ → Cⁿ. Классическая теорема об обратной функции гарантирует обратимость локально, в окрестности каждой точки, где определитель матрицы Якоби не равен нулю. Гипотеза утверждала: если этот определитель — ненулевая константа во всём пространстве, то отображение обратимо глобально, причем обратное тоже полиномиально. Коротко: из «локально всюду» следует «глобально». 87 лет это не удавалось ни доказать, ни опровергнуть.

Опубликованное отображение имеет степень 7 [11]:

F₁ = z(1 + xy)³ + y²(1 + xy)(4 + 3xy),

F₂ = y + 3x(1 + xy)²z + 3xy²(4 + 3xy),

F₃ = 2x – 3x²y – x³z.

Определитель его матрицы Якоби тождественно равен –2, а две различные точки, (0, 0, –1/4) и (1, –3/2, 13/2), переходят в одну и ту же: (–1/4, 0, 0). Отображение не инъективно — обратного не существует. Условие гипотезы выполнено, заключение нарушено.

Проверка не требует доверия ни к автору, ни к компании — разработчику модели. Коэффициенты целые, точки рациональные: и определитель, и совпадение образов проверяются точной арифметикой в любой системе компьютерной алгебры за минуты. При подготовке заметки вычисление воспроизведено независимо — определитель равен –2 тождественно, совпадение образов подтверждается.

Что здесь установлено, а что известно со слов участников? Установлено: свойства самого отображения, они проверяются механически, и происхождение объекта на них не влияет. Со слов автора: кандидата предложила модель. Протокол взаимодействия не опубликован — ни постановка запроса, ни число неудачных попыток, ни доля ручной доводки [12]. Для судьбы гипотезы это безразлично, для оценки возможностей моделей — необходимо.

Статус результата. Для размерностей n ≥ 3 гипотеза опровергнута, для плоскости (n = 2) вопрос остается открытым. Рецензированной журнальной публикации пока нет, но идет машинная формализация: 20 июля в репозиторий formal-conjectures (его поддерживает DeepMind) подан pull request с проверкой опровержения на языке Lean [13]. Кевин Баззард (Имперский колледж Лондона), многолетний куратор формализации математики, сформулировал требование к таким результатам коротко: «Пожалуйста, формализуйте целиком в Lean» [14]. Неформальные тексты от ИИ он не читает.

У результата есть сосед по времени. За полсуток до поста Альпёге та же модель по запросу математика Ахила Мэтью нашла контрпример к вопросу Гротендика о конечных плоских групповых схемах — и сама же формализовала его в Lean файлом на 1076 строк. Баззард, по собственным словам, просматривал этот файл в том числе на предмет того, что код не удаляет файлы с жесткого диска. Lean — полноценный язык программирования, и машинный текст на нем проверяют как код [14].

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

10. fastcompany.com/91577272/jacobian-conjecture-anthropic-ai-levent-alpoge

11. johndcook.com/blog/2026/07/21/jacobian-conjecture/

12. theconversation.com/hello-there-the-jacobian-conjecture-is-false-thanx-why-a-tiny-social-media-post-has-mathematicians-rethinking-ai-283883

13. github.com/google-deepmind/formal-conjectures/pull/4474

14. xenaproject.wordpress.com/2026/07/20/human-mathematicians-are-being-outcounterexampled/