➗ Стартап Axiom решает Putnam на 12/12 и переопределяет путь к AGI через формальную верификацию

Семимесячный стартап Axiom Math в 2025 году решил все 12 задач престижного экзамена Putnam (8/12 в лимите времени) — результат выше, чем у лучших студентов (110/120) и ближайшей AI-системы DeepSeek (103/120). Медианный балл на Putnam обычно 0–1. Но для CEO Axiom Карины Хонг это лишь начало: она считает, что код — необходимое, но недостаточное условие для AGI.

Ключевая идея Axiom — «верифицированный AI» через формальные доказательства в системе Lean. В отличие от статистических методов вроде GRPO, Lean-верификатор даёт абсолютно надёжный сигнал подкрепления: доказательство либо верно, либо нет. Это радикально повышает эффективность обучения и качество результатов.

На бенчмарке Verina (генерация кода + доказательство корректности) Axiom достиг 99% (187/189) против 4.9% у OpenAI o3. Стартап также открыл инструментарий AXLE — набор интерактивных Lean-приложений для исследования и проверки математических доказательств.

#AI #Science #Mathematics #Axiom #Lean

➗ Claude впервые формализовал великую теорему Ферма в Lean

Anthropic сообщила, что её ИИ-модель Claude практически автономно за 11 дней создала первую полностью проверяемую компьютером формализацию великой теоремы Ферма. Результат записан на языке Lean — всего Claude написал 13 миллионов строк кода и доказал 29 500 промежуточных теорем. Готовое доказательство опубликовано на GitHub.

Формализация переводит математическое рассуждение в вид, который компьютер может проверить автоматически, без опоры на «очевидные» шаги, пропускаемые в человеческих доказательствах. Оригинальное доказательство Эндрю Уайлса 1995 года занимало 129 страниц, а его проверка заняла месяцы. Сообщество математиков ожидало, что формализация такой сложной теоремы займёт годы — один лишь «чертёж» проекта насчитывал 86 страниц. Claude справился за полторы недели, а профессор Кевин Баззард, лидер сообщества по формализации FLT, назвал результат экстраординарным и пригодным для дальнейшего построения.

Практическая значимость — в верификации будущих математических открытий. Проверка новых результатов у людей может занимать годы; ИИ-формализация способна превратить её в автоматизированную процедуру, как проверку вычислений на калькуляторе. Anthropic подчёркивает, что в данном случае новизна не в самой математике, а в надёжности: доказательство теперь проверено на уровне аксиом.

#AI #Claude #Lean #Math #Formalisation

🌐 AlphaProof Nexus от Google DeepMind решил десятки открытых задач и прошёл рецензирование

Новое исследование Google DeepMind, опубликованное в Science, описывает систему AlphaProof Nexus, которая самостоятельно справилась с рядом нерешённых математических проблем. Она закрыла 9 из 353 открытых задач Эрдёша - две из них оставались нерешёнными 56 лет. Решения были выложены в открытый доступ ещё до выхода статьи.

В основе системы - Gemini 3.1 Pro, который пишет и правит доказательства на формальном языке Lean. Lean проверяет каждый черновик после правки, а сообщения об ошибках задают направление следующей попытки. Для сложных подзадач система может обращаться к специализированному инструменту AlphaProof, хотя, по данным DeepMind, 9 задач Эрдёша были решены и без него. Помимо этого AlphaProof Nexus доказал 44 гипотезы из базы целочисленных последовательностей OEIS, закрыл открытый вопрос в алгебраической геометрии и улучшил известную границу в min-max оптимизации - методе, применяемом при обучении некоторых ИИ-моделей.

Работа вышла на фоне спора о роли ИИ в математике: OpenAI ранее выложила сотни ИИ-доказательств на GitHub вместо отправки в журналы, а Ассоциация человеческой математики во главе с Теренсом Тао призывала к бойкоту. DeepMind, в отличие от этого, провёл свои результаты через рецензирование.

🎨 qvabo.studio/tg · картинки и видео

#AI #GoogleDeepMind #AlphaProof #Mathematics #Lean