Решение каждой задачи в одном из самых сложных тестов по математике обычно стоит десятки тысяч долларов. NEAR AI сделал это всего за 111 долларов.
6 сентября 2026 года сооснователь NEAR Protocol Алекс Скиданов объявил, что открытый агент Lean проекта решил все 672 задачи в бенчмарке PutnamBench, наборе задач, взятых из математической олимпиады Уильяма Лоуэлла Патнэма. Общая стоимость: 111 долларов. Второй по стоимости известный результат стоил в 250 раз больше.
Что такое PutnamBench и почему это важно
Соревнование Путнама — самое престижное студенческое математическое соревнование в Северной Америке. Результат в ноль — нечто обычное, даже среди блестящих студентов. Экзамен создан, чтобы сломать вас.
PutnamBench, представленный в 2024 году, берет эту традицию сложности и превращает ее в формальный набор оценок для ИИ-доказателей теорем. В бенчмарке содержится 672 задачи, закодированные на Lean 4 — языке помощника по доказательствам, требующему математических аргументов, записанных с машинной точностью. Доказательство, содержащее логические неточности, сразу отклоняется, без частичного зачета.
До результатов NEAR AI агенты, пытающиеся пройти PutnamBench, часто требовали тысячи вызовов вывода на каждую задачу. Расходы на вычисления быстро накапливались, и полные запуски тестового набора стоили в общей сложности от 10 000 до 25 000 долларов для ведущих систем.
Агент NEAR AI завершил весь набор из 672 задач за 111 долларов.
Почему разница в стоимости — это настоящая история
При стоимости от 10 000 до 25 000 долларов за полный цикл только небольшое количество организаций могли позволить себе итерации, эксперименты и улучшение своих конвейеров доказательства теорем. При стоимости в 111 долларов эта картина полностью меняется.
Быстрое развитие результатов PutnamBench между 2025 и 2026 годами уже определялось агентными рабочими процессами, объединяющими крупные языковые модели с движком проверки доказательств Lean. Подход NEAR AI расширяет эту модель, добавляя уровень эффективности, которого сообщество бенчмарков ранее не видело.
NEAR AI позиционирует это достижение в рамках более широкой инфраструктурной концепции, основанной на так называемом IronClaw — фреймворке, ориентированном на конфиденциальные и проверяемые ИИ-системы. Возможность формальной верификации напрямую соответствует этой концепции: если вы можете доказать корректность математического аргумента на уровне машины, вы получаете основу для ИИ-систем, выходы которых можно независимо аудитировать, а не полагаться на веру.
Решение NEAR Protocol сделать Lean-агент открытым исходным кодом усиливает его значимость. Проприетарные инструменты, обеспечивающие 250-кратное преимущество в стоимости, обычно остаются проприетарными. Открытие исходного кода агента означает, что методология доступна для проверки, расширения и использования всеми.