9 октября 2026 г.
Google DeepMind решил 9 открытых задач Эрдёша: каждое доказательство проверено Lean
AlphaProof Nexus, обновлённый AlphaProof от Google DeepMind, решил 9 из 353 открытых задач Эрдёша: препринт вышел 21 мая 2026, а статья в Science опубликована 8 октября. Тем же методом доказано 44 из 492 открытых гипотез OEIS.
Раньше языковая модель полагалась на правдоподобные рассуждения, а они ломаются на логических ошибках. Здесь доказательство записано на языке Lean, и каждый шаг проверяет сам Lean, а не вера в ответ нейросети.
Gemini 3.1 Pro предлагает стратегии доказательства, а несколько независимых агентов пробуют разные идеи, оформляют их в конструкции и проверяют результат. На одну задачу уходит несколько сотен долларов вычислений.
Не хотите разбираться сами? Внедряем ИИ в ваш бизнес: задачи без лимита, одна цена в месяц, отмена в любой момент.
Проверить можно. Доказательства лежат в открытом репозитории google-deepmind/alphaproof-nexus-results. Для проверки нужен Lean 4, затем команды `lake exe cache get` и `lake build`. Исходный код системы в репозитории не выложен, поэтому повторить решение самой системой по нему нельзя.
По препринту без решения остаются 344 из 353 задач Эрдёша.
Первоисточник