Иногда за одни сутки в ленте X собираются два примера, которые на первый взгляд не имеют друг с другом ничего общего: разговорная правка 3D-сцены в Blender и формальная верификация одной из самых знаменитых теорем в истории математики. Но оба случая — про одно и то же: агенты Claude Code всё увереннее берут на себя задачи, где раньше требовался либо художественный вкус, либо годы экспертной работы, а не просто написание кода по спецификации.
Blender как полигон для агентной итерации
Саймон Уиллисон опубликовал новый TIL о связке коду-агентов с уже установленным Blender на macOS: модель получает доступ к приложению и рендерит сцену «пеликан на велосипеде» — свой неофициальный бенчмарк для сравнения моделей. Интересна не сама картинка, а процесс: пользователь трижды подряд просит агента улучшить результат — добавить фон, добавить «изюминку», сделать «значительно лучше» — и каждый раз получает осмысленную правку без переписывания промпта с нуля.
Это ключевое отличие агентного подхода от разового запроса к модели генерации изображений: агент держит контекст сцены, файлы проекта и API Blender одновременно, поэтому правки накапливаются, а не стартуют заново. Уиллисон отмечает, что результат оказался заметно сильнее его прежних экспериментов с играми на других моделях — не потому, что сама модель радикально умнее, а потому, что итеративный цикл «правка → рендер → следующая правка» позволяет агенту довести черновой набросок до приличного вида за несколько шагов.
Теорема Ферма: агент как соавтор формализации
Второй пост — ретвит Бориса Черни с анонсом Anthropic — работает на порядок серьёзнее. Проверка сложного математического доказательства человеком-рецензентом может занимать годы; формализация — перевод рассуждения в код, который проверяют ассистенты вроде Lean, — способ снять эту нагрузку. В прошлом месяце Claude завершил первую формализованную запись доказательства Великой теоремы Ферма — задачу, которую эксперты оценивали в «многие годы» работы. Это крупнейший из когда-либо написанных Lean-доказательств.
Теорему доказал Эндрю Уайлс в 1995 году, спустя более 350 лет после формулировки — но доказать не значит формализовать. Итоговый Lean-код Anthropic превышает 13 миллионов строк и по пути доказывает ещё 29 000 вспомогательных теорем из областей математики, которые прежде вообще не были формализованы. Anthropic описывает это как шаг в многовековом процессе укрепления основ математического знания — на плечах трёх столетий математиков и сотен участников проектов Lean и Mathlib.
Что объединяет два кейса
Разница масштабов огромна — рендер шуточной сцены и верификация фундаментальной теоремы вроде бы из разных вселенных. Но механизм один: агенты Claude Code не заменяют экспертизу единым «правильным» ответом, а итеративно доводят промежуточный результат до нужного состояния, удерживая контекст задачи между шагами. В Blender это выражается в разговорных правках сцены, в Lean — в способности пройти миллионы строк формальных выкладок, не теряя нить рассуждения.
Для разработчиков и исследователей это практический сигнал: если задача поддаётся итеративной проверке — визуальным рендером, компилятором, доказательным ассистентом, — агент способен закрыть её эффективнее, чем разовый запрос к модели. Формализация теоремы Ферма при этом не просто эффектная демонстрация: это заявка на то, что подобные агенты в обозримом будущем возьмут на себя рутинное рецензирование математических работ, которое сейчас физически не успевают делать люди.
Добавить комментарий