Тысяча агентов Claude Fable 5.2 за 30 часов формализовала доказательство Великой теоремы Ферма в Lean. В таком же эксперименте Opus 5.5 осилила 26% формализации за первые 18 часов и почти не продвинулась за оставшиеся 12. Anthropic опубликовала оба прогона в анонсе Fable 5.2 и Mythos 5.2.
Что проверял Lean
Великая теорема Ферма утверждает, что для целого n > 2 у уравнения aⁿ + bⁿ = cⁿ нет решений в положительных целых числах. Доказательство Эндрю Уайлса было опубликовано в 1995 году после исправления пробела совместно с Ричардом Тейлором. Задача агентов состояла в том, чтобы записать математический аргумент на языке, который может проверить компьютер.
В Lean утверждение задаётся типом, а доказательство представляет собой терм этого типа. Тактики строят терм доказательства, ядро проверяет его тип. Чтобы применить лемму, нужно доказать её предпосылки. Если нужной леммы нет в библиотеке, её тоже приходится записывать и доказывать в Lean.
В сентябрьском эксперименте Anthropic отслеживала эти зависимости в Prove2Me. Платформа хранила направленный ациклический граф утверждений. По нему агенты видели, какие леммы уже доказаны и где можно продолжать работу параллельно. Тот прогон занял 11 дней, а в итоговое доказательство вошли 29 500 промежуточных теорем. Отдельная проверка подтвердила, что финальная формулировка совпадает с формулировкой в Mathlib. Описание сентябрьского эксперимента.
Тысяча агентов и один запуск на модель
В новом эксперименте Fable 5.2 получила короткие стартовые инструкции и список промежуточных утверждений, по которому оценивали прогресс. По данным Anthropic, агенты сами распределяли работу и обходились без математических справочников. Люди вмешивались редко. По сравнению с сентябрьским экспериментом число токенов, затраченных на действия, сократилось втрое, а формальный текст доказательства получился в семь раз короче.
Для Opus 5.5 Anthropic использовала ту же конфигурацию примерно с тысячей агентов. Обе команды через 18 часов возобновили работу с сохранённого состояния. На графике в анонсе по одному прогону каждой модели. В сентябрьском эксперименте использовали другую модель и другую схему координации. График и условия эксперимента.
Миграция с Python на Rust и прототип ОС
Внутри Anthropic команда агентов на ранней версии Fable 5.2 перенесла критичный сервис с Python на Rust. По данным Anthropic, время запуска сервиса сократилось примерно в 26 раз.
В другом эксперименте Fable 5.2 восемь дней координировала работу более тысячи субагентов над прототипом операционной системы. Они начали с пустой папки и получили систему, которая загружается на ноутбуке. У неё есть ядро, драйверы диска, клавиатуры и сети, файловое хранилище, оконный интерфейс и установщик.
На FrontierCode 2.0 у Fable 5.2 получилось 49,1% на уровне усилия Xhigh против 32,4% у Fable 5.1 с той же настройкой. На том же тесте Fable 5.2 в режиме High набрала примерно столько же, сколько Opus 5.5 в режиме Max. Решение одной задачи обходилось примерно вдвое дешевле. Методика и таблица результатов.
Чем Mythos отличается от Fable
У Fable 5.2 и Mythos 5.2 одна базовая модель. У Fable действуют дополнительные ограничения на высокорисковые задачи по кибербезопасности и биологии. Mythos доступна проверенным организациям через программы Anthropic для специалистов по безопасности и биомедицинским исследованиям.
На внутреннем тесте CVE Rediscovery Mythos 5.2 нашла 89,6% уязвимостей против 78,3% у Mythos 5.1 и 81,3% у Opus 5.5 с отключёнными защитными ограничениями. В октябрьском прогоне было 1829 уже опубликованных CVE. Моделям давали версии проектов до исправления, чтобы проверить, сколько известных уязвимостей они найдут самостоятельно.
API, скорость и цена
В API Claude Platform модель доступна под именем claude-fable-5-2. Fable 5.2 доступна также через AWS, Google Cloud и Microsoft Azure. Базовый тариф для обеих моделей составляет $8 за миллион входящих токенов и $40 за миллион исходящих. Anthropic заявляет, что по сравнению с версией 5.1 скорость генерации выросла до 30%. В Fast Mode токены генерируются до 2,5 раза быстрее, тариф составляет $16 за миллион входящих и $80 за миллион исходящих. Официальный анонс Anthropic.
Комментарии (33)
Dhwtj
09.11.2026 19:18Конский прайс за задачу
https://artificialanalysis.ai/models/releases/claude-fable-5-2
Dron007
09.11.2026 19:18Не очень большая проблема, учитывая что "стоимость выполнения задач ИИ при сохранении одинакового уровня качества снижается примерно в 3,5–13 раз в год. Причём для сложных задач программирования, выполняемых LLM-агентами, есть отдельная оценка — в 3,6 раза в год." по исследованиями epoch.ai.
andrey_snegovik
09.11.2026 19:18До 19 ноября входит в недельные лимиты в Claude подписке, идём пробовать!
edo1h
09.11.2026 19:18Claude Fable 5.2 формализовала теорему Ферма за 30 часов
…
Тысяча агентов Claude Fable 5.2 за 30 часовто есть всё-таки не 30, а 30 000 часов
glupiyyashik
09.11.2026 19:181) Дикий прайс за задачу, если судить по агрегированным табличкам https://www.gptunnel.ru/ru/blog/claude-fable-5-2
2) В некоторых задачах на уровне опуса или карбона (который еще не вышел, ага)
3) Откатывает на более слабые модельки в случае "чувствительных запросов"
4) Отзывы чела который ее чуть ли не безлимитно тестил тоже не шибко впечатлили
Ощущение, что модель скорее пошла вширь (робототехника и тд) (ну ладно, еще наука), нежели впечатляет каким-то прогрессом в классических задачах
StandAlone007
09.11.2026 19:181) Дикий прайс за задачу, если судить по агрегированным табличкам https://www.gptunnel.ru/ru/blog/claude-fable-5-2
Ну скажете тоже - дикий. Вы же не видели их внутренние бухгалтерские документы? Ну вот, и (почти)никто не видел. Так что надо постепенно привыкать, график будет идти вправо и вверх.
BugM
09.11.2026 19:18Дикий в смысле что нет смысла столько платить за подавляющую часть задач. Дипсик сделает не хуже и на порядки дешевле. И череп измерять не будет в процессе.
glupiyyashik
09.11.2026 19:18ну вот поэтому дарио и ко и борятся с локальным инференсом)) то они хотят определенные правила регулирования отрасли ввести, то страшилки выпускают, как локальные ллм могут перезаражать всё вокруг, + при попытке улучшить локальную нейронку сброс до более простой модели идёт
короче идеальные условия - китай под запретом в гос учреждениях сша , локальные модельки под запретом + другие ограничения)
Вверх и вправо наверное зависит от того, насколько получится задавить всех этих "понаехов" по типу дипсика и квена
predpremi
Впечатляющее достижение, что тут говорить - формализовать теорему Ферма не каждый день увидишь. Но я, как человек, который сам запускал проекты на нейросетях, сразу задаюсь вопросом: какая реальная ценность за этим стоит? И сколько стоили эти 1000 агентов, работающих 30 часов? Пока это похоже на дорогую демонстрацию возможностей, а не на инструмент с понятной юнит-экономикой или реальным спросом на рынке. Мне всегда интересно, как такая мощь конвертируется в окупаемость.
swanrnd
Это наука. Часто дорого и не факт, что пригодится.
Если брать Великую Теорию Ферма, то она бесполезная для практике. Но ради нее было придумано хороших технологий и тому подобное.
Теорема красивая значимая и поэтому на ней довольно логично проводить вещи.
Если наладить процесс, то можно те же заработки применить на другие задачи, с практической выгодой. Ну пример, малая теорема Ферма основа криптографии.
Vytian
Эвристической ценности хотелось бы... а тут предлагают очередной Монте-Карло. Практическая польза, конечно, есть, но съеденным чижиком отдает.
Flux
Конкретно это - не наука, это поддержание информационного фона и нагон хайпа перед IPO, как раз ради того чтобы потенциальные
лохиинвесторы думали как вы, а не как гражданин которому вы отвечаете.Так сказать, фрейминг мышления - думайте о классных демках, "прорывах" и невероятных будущих перспективах, а не о том сколько это стоит, что за продукт вам продают, какие гарантии его функционирования вы получаете и как вообще этот продукт может быть вам полезен, если он вообще вам полезен.
Как только ранние инвестора выведут деньги после IPO вся эта карусель "открытий", "взломов" и прочих чудес немедленно прекратится.
Spaceoddity
А что тут может пригодиться? Само доказательство и так должно быть полностью формализовано (иначе это и не доказательство). Его просто на служебный язык перенесли...
Dron007
Как это "что может пригодиться"? В математике постоянно так происходит, что то, что сейчас кажется бесполезным, потом находит применение, как и в науке в целом. Тут идет отработка перевода неформализованных математических описаний в формализованное Lean описание, как я понимаю. Процесс нетривиальный. Все эти наработки могут быть использованы в других доказательствах, расширяя покрытие, созодавая новые библиотеки. Полагаете, это не нужно?
Spaceoddity
Это не математика! Это прикладное программирование. И какая тут "наработка"? Чего? Дали промт и получили формализацию?
LinkToOS
Формализация чего-либо в системе интерактивных доказательств, это задача на стыке математики и программирования. Одной из целей является развитие и улучшение самих систем интерактивных доказательств теорем.
Попытка формализации в Lean, это одновременно проверка пригодности Lean для анализа данной математической проблемы. И если формализовать не получается, то всегда возникает вопрос - в чем причина? Это ошибка математика, или ошибка программиста, или ограничение самой системы? Если формализовать математическую проблему не удается, то это может означать что сама система Lean требует изменений и дополнений.
Так что вопрос здесь не “зачем подтверждать конкретно теорему Ферма”, а более общий - “зачем нужны системы интерактивных доказательств теорем”, и какие у них перспективы практического применения? Приведет ли их развитие к созданию универсальной электронной системы, которая заменит всех математиков?
Spaceoddity
Именно в этом. Потому что вопрос тут - "что такого может доказательство ВТФ, чего не может любое другое доказательство?".
Проверили? Работает? Отлично. Как дальше будем это использовать? Проверять на следующей? Плюс неплохо бы проверить саму корректность формализации, а не кивать автоматически "нейросеть смогла".
LinkToOS
Одной из целей является развитие и улучшение самих систем интерактивных доказательств теорем.
Spaceoddity
Звучит, как по мне, довольно обтекаемо и пафосно. Скорее "демонстрация возможностей нейросетей". Потому что не сегодня-завтра, эту прослойку в виде "системы интерактивного доказательства" возьмут и выкинут за ненадобностью))
Yarus23
Да какая там наука? 29 тыс промежуточных теорем. Ни один математик никогда не разберется. Люди доказывают да, дольше, но адаптированно под людей с возможностью понимания и контроля
MEGA_Nexus
Тысячи людей прочитали новость. В ней сказано, что Fable 5.2 очень умная нейросетка и может даже формализовать теорему Ферма. Круто. Сотня пользователей купит себе токенов или подписок на Fable 5.2, чтобы решать свои более простые задачи, т.е. понесут свои деньги Anthropic.
Инвесторы прочитают эту новость и поймут, что Fable 5.2 очень умная нейросетка и может даже формализовать теорему Ферма. Круто. Позже инвесторы также узнают, что сотня новых пользователей купили себе токенов и подписок на Fable 5.2, а значит Fable пользуется популярностью, поэтому инвесторам следует прикупить немного акций Anthropic, т.е. они понесут свои деньги Anthropic.
Чтобы цена акций была выше, нужно заранее подогреть к ним интерес. А значит будет много позитивных новостей о том, что Claude где-то занял первые места, кому-то очень сильно помог или смог решить важные для человечества задачи. Чем выше хайп, тем выше спрос на акции, тем выше их цена и тем больше иксов смогут сделать ранние инвесторы Anthropic. Так что те, чьи деньги ранее сжигал Anthropic, смогут выйти в хороший плюс и вернуть всё с большими бонусами. А новые покупатели акций Anthropic по факту будут спонсировать новое сжигание денег до того момента, пока Anthropic не выйдет на самоокупаемость и реальную прибыль.
LinkToOS
Все верно. Сейчас решается задача не дать проекту утонуть. Новость об успешной “формализации теоремы Ферма” полезна для рекламы.
Но и при устойчивом финансовом положении Anthropic, подобные новости все равно были бы уместны, ради той же рекламы. И это оправдало бы “формализацию теоремы Ферма”.
И даже при отсутствии нужды в рекламе, “формализация теоремы Ферма” имела бы смысл для исследования возможностей моделей, в рамках развития моделей.
Так что для самих Anthropic “формализация теоремы Ферма” имела бы смысл в любом случае.
edo1h
примерно нисколько
я думаю, что это эти 30к агенто-часов — малая доля того, что anthropic потратила на внутренние тесты новой версии fable
predpremi
Ну учитывая миллиардные раунды, поднимаемые на работу минусового сервиса - кажется что "нисколько" это точно не себестоимость.
edo1h
предоположим, вы велосипедист и по плану тренировок вам нужно 3 раза в неделю ездить на 100км.
вы решили съездить в соседную деревную в 40км от места, где вы живёте.
сколько стоит эта поездка для вас? да нисколько, вы бы так и так эти 100км проехали.
Spaceoddity
Но вы уже за эту неделю накрутили 300км...
Atreides07
Собственно все так и есть - это демонстрация возможностей и в этом и смысл этого проекта. Фактически это вложение в рекламу и демонстрация для инвесторов. Но в истории немало примеров как компании развивали науку просто исходя из корыстных целей продемонстрировать себя как технологического лидера. Например в свое время AT&T создала Bell labs и учёные работавшие на деньги корпорации получили 9 нобелевских премий и создали такие штуки как транзистор который фундаментально повлиял на всю электронику и открыли реликтовое излуние. Считал ли AT&T юнит экономику открытий которые возможно сделают ученные в их лабораториях? Или практическое применение и юнит экономику реликтового излучения? Вряд ли - они просто вкладывались в маркетинг и бренд компании.