Возвращаюсь ко вчерашней истории с 722 доказательствами, потому что она шире математики.

Смотрите, что там произошло. Проверка подешевела почти до нуля: Lean прогоняет формальное доказательство за секунды и говорит «верно» или «неверно». А осмысление не подешевело совсем. Прочитать 722 работы, понять, что в них нового, и встроить это в здание математики — по-прежнему человеческий труд, и его столько же, сколько было.

Получается перекос. Генерация — быстро. Проверка — быстро. Понимание — с той же скоростью, что и сто лет назад.

Поэтому лауреаты возмущаются не результатом, а тем, что из 722 работ почти нигде не видно хода рассуждения. Им отдали ответы без решения. Формально корректные — и непригодные, чтобы на них что-то строить дальше.

Мне это кажется знакомым по совсем другой области.

Когда агент приносит готовый код, который проходит тесты, у вас ровно та же ситуация. Корректность проверена машиной. Понимания, почему сделано так, нет ни у кого. И пока всё работает, разницы никакой.

Разница появляется в тот день, когда это надо менять.

#мысли #работа