ny_quant

using the formal verification language Lean, 8 of which within the exam time

По ссылке приводятся все решения. Впечатляет.

Из комментариев на LinkedIn (дать ссылку не получается):

Looking at the GitHub repo, problem B5 took 354 minutes and 18M tokens. B6 took 494 minutes and 21M tokens.

Интересно, каких ресурсов потребовало бы сегодня решение задачи, которая занимает у хорошего профессионального математика, скажем, месяц. И как далеко мы до того как ИИ будет делать это быстрее. Возможно, не так уж и далеко, если до этой стадии можно добраться собирая относительно низко висящие плоды. А может быть туда ведет такая экспонента, что всей энергии человечества не хватит, чтобы обучить такую модель. Или может быть где-то впереди все же есть твердая стена, которую в лоб не пробить. Кто знает.