Google DeepMind опубликовал результаты работы AlphaProof Nexus — системы, которая автономно решила девять открытых задач Эрдёша, включая две, не поддававшиеся математикам 56 лет. Каждое решение обошлось в несколько сотен долларов вычислений. Уровень успеха — 2,5% от всего корпуса атакуемых задач. Немного. Но именно эти 2,5% содержат то, что человечество не могло доказать полвека.
Контекст
Пол Эрдёш — венгерский математик, написавший совместные работы с рекордным числом авторов и оставивший после себя сотни открытых задач с денежными премиями за решение. Эти задачи — не пазл для подростков: они касаются комбинаторики, теории чисел, теории графов. Часть из них не решена до сих пор. AlphaProof — линейка систем DeepMind, работающих с формальной математикой.
Ключевое отличие подхода DeepMind от конкурентов: система использует компилятор Lean. Lean — это язык для формальной верификации доказательств: каждый шаг проверяется автоматически, и система не может «придумать» обход. OpenAI в своих математических системах работает на естественном языке, что быстрее, но менее строго — LLM способна генерировать убедительно звучащий, но логически дырявый аргумент.
AlphaProof Nexus атаковал именно открытый корпус — задачи, у которых нет известного решения. Это принципиально иная позиция, чем соревновательная математика типа IMO, где ответ уже существует и система его ищет.
Аналитика
2,5% успеха звучат скромно, но сама постановка делает этот показатель значимым. Речь не об экзаменационных задачах с известным ответом, а о настоящем фронтире математики. Человек-математик мог работать над одной задачей Эрдёша годами без результата. Система решила несколько за время одного inference-прогона стоимостью в несколько сотен долларов.
Это важный сигнал о направлении разработки. DeepMind ставит на формальную верификацию, а не на «правдоподобность». В перспективе это означает системы, которые не просто отвечают «похоже правильно» — а дают доказательства, которые можно механически проверить. Для научных вычислений, криптографии, финансового моделирования и инженерных расчётов разница принципиальная.
Параллельно это ставит вопрос: если AI уже закрывает пятидесятилетние открытые задачи — где граница между «AI помогает математикам» и «AI делает математику»? Сейчас система работает на узком участке. Но сдвиг уже происходит, и он структурный.
Кейсы применения в бизнесе
B2B-SaaS стартап с аналитическим ядром. Формальная верификация логики — не только про высшую математику. Если продукт считает риски, оптимизирует маршруты или строит рекомендательные системы, инструменты типа Lean позволяют верифицировать алгоритмическую корректность. Сценарий: интегрировать Lean-проверку на ключевые формулы расчёта прямо в CI/CD — ошибки вылавливаются до деплоя.
Корпорация с legacy-инфраструктурой. В финансовых и страховых компаниях часть расчётных моделей существует как «чёрный ящик» — работает, но никто не может объяснить почему. Подход формальной верификации, которую демонстрирует AlphaProof, открывает путь к аудиту таких моделей: сначала формализуй логику, потом проверь автоматически. Стоимость ошибки в этих индустриях достаточно высока, чтобы оправдать инвестиции.
SMB и локальный бизнес в КР/СНГ. Прямое применение пока далеко. Но косвенно: если AI-системы начинают решать задачи уровня открытых математических проблем, то задачи типа «оптимизировать логистику», «найти аномалии в отчётности», «верифицировать контракт» становятся ещё более доступными для автоматизации. Следующие два-три года — момент встроить аналитический AI в операционку, пока стоимость ещё низкая.
Кейсы в личной жизни
Разработчик. Lean и другие proof assistants уже доступны как инструменты. Если пишешь критическую логику — алгоритмы сортировки, парсеры, финансовые расчёты — попробуй сформулировать свойства функции на Lean и проверить их формально. Это медленнее, чем unit-тесты, но даёт другой уровень гарантий.
Студент или исследователь. AlphaProof и аналогичные системы начинают появляться как инструменты помощи в доказательствах. Если занимаешься математикой, логикой, CS-теорией — следи за экосистемой Lean 4 и Mathlib: сообщество активно, инструменты AI-ассистирования для формальных доказательств развиваются быстро.
Контент-мейкер или science communicator. Тема «AI решает нерешённые математические задачи» — один из немногих нарративов, где можно говорить о реальном качественном прорыве без преувеличения. Аудитория это чувствует. Если делаешь контент про технологии — это материал, который будет работать долго.
Как применить сегодня
- Изучи экосистему Lean 4 — это язык формальной верификации, на котором работает AlphaProof. Есть бесплатный онлайн-туториал и активное сообщество.
- Если ты разработчик — попробуй Lean + Mathlib для верификации одного нетривиального алгоритма в своём проекте. Это расширяет понимание корректности кода.
- Следи за публикациями DeepMind по AlphaProof — это активно развивающаяся линейка, и следующие версии, вероятно, поднимут планку успеха выше 2,5%.
- Для бизнеса: оцени, есть ли в продукте расчётная логика, где ошибка стоит дорого. Именно туда в ближайшие годы придут инструменты формальной верификации, удешевлённые AI.
- Сохрани этот кейс как бенчмарк: несколько сотен долларов за решение 56-летней открытой задачи — это точка отсчёта для разговора о стоимости AI-вычислений в R&D.