AI Axiom solved all Putnam competition problems

[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.

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

Comments

[lemberger]

Что все - не считаю (и во все не вчитывался). Из двух названных - одна тривиальное упражнение на обязательном курсе, другая несложная и скучная. Но главное - они не говорят, каков там вклад людей. Полагаю, что весьма не маленький - вот как Святогородский ниже объясняет.

Сам я, кстати, никаким ИИ ни разу не пользовался.