3) Что, получается БЯМ всесильны?
Т.е. у БЯМ есть только часть так или иначе формализованного контекста, необходимого для решения задачи, а всё остальное это что? Это «интерфейс» или «площадь поверхности» задачи – то, чем она «соприкасается» или «связывается» с окружающим миром. Например, для веб-сервиса такой «площадью поверхности» будет API (в т.ч. между сервисами) с UI. А для математической проблемы это будет применимость решения соответствующей проблемы в окружающем мире. Тут надо уточнить, что математический формализм позволяет путём рекомбинации создавать бесконечное число удовлетворяющих аксиомам утверждений любой сложности и «подчеркнуть» в качестве результата можно любое из этих утверждений, т.ч. чтобы назначить одно из них имеющим какое-то значение, надо понимать применимость такого утверждения в окружающем мире.
Так вот, по «площади поверхности» задачу может верифицировать пока, увы, только человек. И тут возникает любопытный эффект: задача может быть очень «сложной», т.е. требовать для своего решения согласованного учёта большого формализованного контекста, но при этом с очень маленькой «площадью поверхности» – такую задачу можно назвать задачей с «высокой плотностью»; и задача может быть более «простой», т.е. требовать для решения учёта меньшего контекста, но при этом обладать большой «площадью поверхности» – такую задачу можно назвать задачей с «низкой плотностью». Пример задачи с высокой плотностью – решение открытой проблемы математики, пример задачи с низкой плотностью – создание функционально наполненного приложения.
И БЯМли лучше всего подходят именно для решения задач с маленькой площадью поверхности, независимо от их плотности, просто потому, что именно участие человека в процессе является плохо масштабируемым узким местом, а чем площадь поверхности задачи меньше, тем меньше этого участия требуется. Как ни странно, но, похоже, доказать новую теорему с помощью «ИИ» уже очень скоро будет проще, чем написать относительно сложное приложение, т.к. у такого приложения площадь поверхности с ползающими по ней бестолковыми людьми достаточно большая.
Вот такие дела. На самом деле, если меня читают какие-то учёные, вовлечённые в формулирование новых научных утверждений, я настоятельно советую ознакомиться с инструментарием для автоматизированного доказательства теорем, таким как Lean или Rocq, активно наполнять библиотеки доказательного инструментария оцифрованными результатами научной деятельности человечества, а также освоить использование языковых моделей для генерации соответствующим образом формализованных утверждений – именно за этим ближайшее будущее фундаментальной науки. И уплотняем задачи