«Першу серйозну задачу» Ердеша спростовано
3 вересня 2026 року Epoch AI оприлюднила спростування в Lean задачі Ердеша № 1 (1931 рік): множини з n цілих чисел із різними сумами підмножин можуть уміщатися в {1, …, N} з N менше за будь-яку фіксовану частку від 2^n. Спростування знайшов pre-release GPT-6 Astra у прогонах FrontierMath Erdős. Lean його перевірив; за статтею, люди ще не «перетравили» аргумент.
Чому це важливо
Ердеш назвав цю задачу «можливо, моєю першою серйозною»; стаття Epoch вважає її, ймовірно, найдавнішою відкритою задачею Ердеша. Оцінка 2^n/√n знизу трималася від Ердеша й Мозера, а найкращий приклад до того мав N ≤ 0,22002·2^n. Це стан «формально перевірено, людьми ще не розібрано»: він відрізняється від стану гіпотези Ердеша — Шоша, яку люди вже виклали заново.
Стан твердження. Заявлено: стаття Адамчевського й Блума (arXiv 2609.25050, 6 вересня), додаток B.1, і репозиторій github.com/tadamcz/erdos1, створений 3 вересня 21:48 UTC. Формалізовано в Lean: за README, спростування знайшов «автономно» pre-release GPT-6 Astra; основна спроба — конфігурація за замовчуванням, 28 серпня (прогін бенчмарка), $405, 27,1 години; друга, інша, — агент ReAct із більшим бюджетом, 26 серпня, $1384, 84 години; Comparator приймає спростування лише з тим самим твердженням і лише з трьома стандартними аксіомами. Прохід репозиторій не збирав. Перевірено людьми: стаття каже, що формальна перевірка дає впевненість у правильності, але доведення «ще не належно перетравлені», а пояснення на erdosproblems.com — «заповнювачі», доки люди-експерти не підготують звичайну статтю. Блум (другий автор) переформулював аргумент мовою ґраток; його ескіз на сторінці задачі не читано (сторінка № 1 на erdosproblems.com 10 жовтня подає лише умову). Зміст. Скінченна множина A натуральних чисел «дисоційована», якщо суми підмножин усі різні. Ердеш питав, чи завжди N ≫ 2^n, якщо A ⊆ {1, …, N} має n елементів; приклад {1, 2, 4, …, 2^(n−1)} показує, що N ≤ 2^(n−1) можливе. Теорема 1 статті: для будь-якого ε > 0 існують як завгодно великі n і дисоційовані множини розміру n з N ≤ ε·2^n. Аргумент неефективний (не каже, наскільки великим має бути n). README репозиторію додає, що сайт задач указує приз $500; сама стаття цього не каже. Чого запис не стверджує: що людина перевірила аргумент; що прохід збирав доведення.