По мне, тут самое классное, что "массовый параллельный перебор доказательств с приоритезацией по вычислительному бюджету" (10 тыс. агентов, 88 часов и 15 млн. долл. на токены) идея древняя.
Левин, 1973 Universal Search -- математически оптимальный способ искать решение, если есть формальный верификатор.
Шмидхубер, 1995-1997 -- отец самомодифицирующегося поиска в пространстве программ "Discovering Neural Nets with Low Kolmogorov Complexity", да и трансформеров по сути,
затем его же Optimal Ordered Problem Solver 2002.
А сегодня к этой базе просто добавили "интуицию" нейронок, которые не брутфорсят, а угадывают, какая лемма правдоподобна, и эффективность действительно на порядки выше. Ну и мощные инструменты доказательств появились - пруф-ассистанты благодаря Воеводскому.
Лет пять я пишу, что все идеи в computer science закончились к 1980-му, и их сегодня просто развивают и погружают в современную инженерию.
А что сейчас массово заголосили и про рекурсивное самоулучшение нейронок,
так это всё тот же Шмидхубер 2003: Gödel Machine - самореферентная система, которая переписывает саму себя, если может доказать, что новая версия глобально лучше.
А потом Шмидхубер пояснял, как способность к неограниченной саморефлексии и доказуемо полезным изменениям может служить техническим обоснованием феномена сознания, но это уже совсем иная история.
...Смотрю, а Шмидхубер красавчик и сейчас вовсю трудится, научный директор швейцарской лаборатории искусственного интеллекта IDSIA, вовсю пилят AGI :)
В этом году он пояснял за формальную теорию творчества и любопытства(!), похищу его идеи для (Meta) Principles Framework, сразу после LPF.