Формальний пошук доведень закриває дев'ять задач Ердеша
Агент, що генерує доведення в Lean і там же їх перевіряє, автономно розв'язав 9 із 353 відкритих задач Ердеша і довів 44 з 492 гіпотез із енциклопедії цілочислових послідовностей.
Чому це важливо
З'явився знаменник: не кількість закритих задач, а частка від фіксованого відкритого набору, причому кожне доведення перевірено машиною.
Статтю подано на arXiv 21 травня 2026 року, авторів двадцять один, перші — Джордж Цукалас, Антон Ковшаров і Сергій Широбоков. Система поєднує велику мовну модель, що генерує формальні доведення мовою Lean, із перевіркою кожного кроку тим самим Lean: якщо доведення не тримається, його відкидають. Заявлені результати: агент автономно розв'язав 9 із 353 відкритих задач Ердеша і довів 44 з 492 відкритих гіпотез з Онлайн-енциклопедії цілочислових послідовностей. Другий підхід, що чергував генерацію моделлю з перевіркою в Lean, відтворив результати на задачах Ердеша, але виявився дорожчим на найважчих. Робота охоплює комбінаторику, оптимізацію, теорію графів, алгебричну геометрію та квантову оптику. Quanta Magazine приписує цю роботу команді DeepMind із 21 дослідника.