Гіпотезу Ердеша — Шоша доведено в Lean
3 вересня 2026 року Том Адамчевський з Epoch AI оприлюднив доведення гіпотези Ердеша — Шоша в Lean, знайдене pre-release GPT-6 Astra 26 серпня в додатковій спробі з більшим бюджетом бенчмарка FrontierMath Erdős: граф із понад (k−2)n/2 ребер містить кожне дерево на k вершинах. Доведення пройшло перевірку Comparator; до 18 вересня три статті спростили або виклали його.
Чому це важливо
Epoch цитує Чунґ: «одна з найспокусливіших задач екстремальної теорії графів». Доведення коротке: воно рахує пари з порядку вершин і мітки, і сторонні математики вивели його заново та спростили за дні. Це приклад, де правильність підтверджує перевірка в Lean, а не рецензент, і де люди зі свого боку підтвердили аргумент окремо.
Стан твердження. Заявлено: репозиторій github.com/tadamcz/erdos548, створений 3 вересня 21:48 UTC, і PDF доведення («A counting proof for Erdős problem 548», GPT-6 Astra) на erdosproblems.com, змінений 3 вересня 22:20 UTC (сам PDF не читано); стаття Адамчевського й Блума (arXiv 2609.25050, 6 вересня), додаток B.4. Формалізовано в Lean: за README, доведення знайшов «автономно» pre-release GPT-6 Astra в агентній конфігурації з бюджетом $1000 (спроба 26 серпня, $363, 20,5 години роботи, один успіх із кількох спроб), «ніхто не бачив і не спрямовував пошук»; Comparator (Lean FRO) приймає доведення лише з тими самими твердженням і лише з аксіомами propext, Quot.sound, Classical.choice, без sorry; після перенесення з Lean 4.27.0 на 4.28.0 змінено один рядок. Прохід репозиторій не збирав. Формальне твердження перевірив Блум; воно трохи слабше за класичне «більше ніж», коли (k−1)n непарне: README каже це прямо. README каже також, що репозиторій написали ШІ-асистенти за дорученням Адамчевського. Перевірено людьми: Олівер Ріордан і Алекс Скотт (arXiv 2609.15893, 14 вересня) пишуть, що гіпотезу «доведено GPT-6 Astra дуже винахідливим і несподіваним аргументом», дають спрощений варіант і визначають екстремальні графи; Девід Вуд (arXiv 2609.17877, 15 вересня) викладає доведення; Брайс Фредеріксон (arXiv 2609.21159, 18 вересня) дає простіше доведення через випадкові циклічні порядки. Оскарження в прочитаному не знайдено. Зміст. За статтею: для n ≥ k граф на n вершинах із понад (k−2)n/2 ребер містить кожне дерево на k вершинах; Ердеш і Шош висунули гіпотезу 1962 року. Аргумент рахує пари (порядок вершин, мітка j) з ребром v1vj: їх 2m(n−1)!, а для фіксованого дерева T їх не більше C(T) + (k−2)n!, де C(T) = 0, якщо T у графі немає. Дати. Сторінка Epoch від 1 вересня (запис evt-0405) пізніше доповнена додатковими спробами; число спроб на ній (4 для задачі 548) відрізняється від статті v1 (3), тож запис бере числа зі статті. Чого запис не стверджує: що прохід перевіряв доведення; хто з людей вперше прочитав його.