Проблема Эрдёша #1026, впервые сформулированная в 1975 году, получила строгую интерпретацию на сайте задач Эрдёша в сентябре 2025-го — и в декабре была закрыта комбинацией онлайн-дискуссий, AI-инструментов и поиска литературы. Знаменитый математик Теренс Тао опубликовал подробный разбор того, как это произошло, на своём блоге 8 декабря.
В версии Тао это игра: Алиса раскладывает монеты по n кучкам, Боб выбирает монотонную подпоследовательность кучек и забирает их. Вопрос — какая доля монет гарантируется Бобу при любой стратегии Алисы? Математически вводится величина c(n), и базовая интуиция даёт масштаб порядка 1/√n, но дальше речь идет уже про точные значения для каждого n. Исходная формулировка Эрдёша была расплывчатой, и только в сентябре 2025 года модератор сайта Томас Блум принял конкретную интерпретацию задачи как валидную.
В первые часы обсуждения 12 сентября участники получили нижние оценки через результат Ханани 1957 года и выдвинули гипотезу c(k²)=1/k для квадратов. Важная оговорка: как обнаружилось уже после решения, эта ключевая оценка для квадратов уже встречалась в литературе — в статье Tidor, Wang и Yang 2016 года. Но в онлайн-обсуждении она не всплывала, и математики застряли на этом этапе почти на три месяца. Этот этап вновь подсвечивает проблему, когда полезные знания теряются в огромном количестве научных статей и работ.
7 декабря Борис Алексеев, проводивший систематическую проверку проблем Эрдёша с помощью AI-инструментов, подключил Aristotle — "математический суперинтеллект" компании Harmonic. Aristotle автономно превратил гипотезу c(k²)=1/k в верифицируемое доказательство на языке Lean, сведя часть рассуждений к задаче упаковки прямоугольников. Это автоматизировало путь от гипотезы к формальной верификации — не "магическая кнопка", но существенное ускорение процесса.
На следующий день, 8 декабря, Теренс Тао применил AlphaEvolve — эволюционный ИИ от Google DeepMind для численной оптимизации. Задача была найти экстремальные последовательности чисел, дающие минимальное значение c(n). За час работы AlphaEvolve выдал паттерн, который никто не увидел за три месяца дискуссий: числа выстроились в структуру, из которой Борис Алексеев сформулировал общую формулу c(k²+2a+1) = k/(k²+a) при ограничениях −k ≤ a ≤ k. Дальше математики оформили это в полноценные доказательства с явными конструкциями для верхних границ.
Финальный поворот случился, когда ИИ-поиск по литературе через Лоренса Ву вывел на работу Baek, Koizumi и Ueoro 2024 года по оси-параллельной упаковке квадратов — она дала недостающий элемент для завершения аргумента. Терри Тao подводит итог: рабочая схема современной математики — люди формулируют и связывают идеи, ИИ ускоряют перебор, формализацию и поиск литературы, а результат получается из их сцепки. Это уже не первый случай решения проблемы Эрдёша с помощью ИИ за последние месяцы.
P.S. Поддержать меня можно подпиской на канал "сбежавшая нейросеть", где я рассказываю про ИИ с творческой стороны.
