Математики решили задачу Эрдёша №123. В ней для попарно взаимно простых чисел (a, b, c > 1) рассматриваются числа вида (a^i b^j c^k) ((i, j, k \ge 0)). Нужно выяснить, можно ли каждое достаточно большое целое число представить как сумму различных таких чисел, причём ни одно слагаемое не должно делиться на другое. Последнее условие — это и есть главная трудность.
Обычная индукция не работала: чтобы получить представление для всех чисел, сперва надо было построить интервал ([N, CN]), а потом «размножить» его с помощью вычитания и деления. Но сам интервал упорно не строился. Известные методы давали арифметические прогрессии примитивных сумм, но с большим начальным смещением и малым отношением верхней границы к нижней. Этого не хватало для индукции.
Ключевая идея — работать на одном однородном экспонентном уровне (i+j+k = D). На таком уровне любые два различных монома не делят друг друга, так что условие примитивности выполняется автоматически. Задача сводится к чисто аддитивной комбинаторике на подмножествах.
Используя конструкцию реберного кода (edge-code), авторы получили набор примитивных подсумм с разными остатками по модулю (c^n) и ограниченным переносом. Применив теорему ван дер Вардена (полученную из теоремы Хейлса — Джуэтта через библиотеку Mathlib), удалось построить сколь угодно длинные точные арифметические прогрессии примитивных однородных сумм.
Затем с помощью специальных весов (A^{M-r} B^r) эти прогрессии превратили в большой интервал на решётке с шагом (abc \cdot d). Чтобы превратить решётчатый интервал в обычный последовательный, использовали примитивные коррекции на трёх координатных гранях. Их размер оказался пренебрежимо мал по сравнению с шириной решётки.
Самое важное — «внутренняя оболочка» (optional interior shell). На том же однородном уровне оставались неиспользованные мономы. Их можно опционально добавлять к уже построенному интервалу, не меняя его нижнюю границу. Каждый такой моном не больше ширины интервала, и вместе они дают массу, растущую как (\Omega(M B^M)), при том что нижняя граница — (O(B^M)). Отношение верхней границы к нижней растёт линейно по (M). Это позволяет для любого (R > 1) и любого порога построить интервал ([N, RN]) из примитивных сумм.
Теперь индукция заработала: если такой интервал с фиксированным (C > 1) уже есть, его можно размножить на все числа. Доказательство завершили для упорядоченных оснований (1 < a < c < b), а перестановкой экспонент — и для всех остальных троек.
Всё формализовано в Lean 4 с Mathlib. Финальная теорема называется Erdos123.erdos_123. Линтер показал только стандартные аксиомы propext, Classical.choice, Quot.sound — никаких sorryAx. Отдельно отмечено, что формулировка со слабым неравенством (a,b,c \ge 1) ошибочна для тройки ((1,1,1)), но в доказательстве используется строгое (>1).