Першу задачу Ердеша закрито ШІ автономно
На arXiv з'явився людський виклад формального доведення в Lean, створеного зв'язкою GPT-5.2 Pro і Aristotle від Harmonic. У анотації сказано, що це перша задача Ердеша, яку вважають повністю розв'язаною ШІ автономно.
Чому це важливо
Уперше названу відкриту задачу зі списку Ердеша закрила машина, і відповідь перевіряється в Lean, а не залежить від судження рецензента.
Статтю подав Нат Сотанапан 12 січня 2026 року, остання редакція — 26 січня. Доведення отримала зв'язка двох систем: GPT-5.2 Pro від OpenAI дала неформальний аргумент, Aristotle від Harmonic звела його до формального доведення в Lean; обома керував Кевін Баррето. Сама стаття — це переклад формального доведення у звичайний математичний виклад, щоб його могли читати люди. Математичний зміст: для нескінченно багатьох трійок, де a!b! ділить n!k!, різниця k = a + b - n має логарифмічний порядок, тобто лежить між C1·log n і C2·log n. Перед цим, 4 січня, Баррето оголосив результат публічно, але учасники форуму зауважили, що формулювання задачі неоднозначне, і спершу вважали доведення частковим; аргумент довели до потрібної версії наступними днями.