17 октября 2026 г.
AlphaProof Nexus: агент Google DeepMind закрыл 9 открытых задач Эрдёша, доказательства проверяются машиной
Агент Google DeepMind решил 9 из 353 открытых задач Эрдёша, две из них висели 56 лет. На каждую решённую задачу уходило несколько сотен долларов вычислений. Препринт вышел на arXiv 21.05.2026.
Раньше эти две задачи стояли открытыми 56 лет. Теперь агент закрыл их, и каждое доказательство записано на Lean. Заодно агент доказал 44 из 492 гипотез OEIS и закрыл 15-летний вопрос о функциях Гильберта в алгебраической геометрии.
Как устроен. Субагенты-доказатели работают на Gemini 3.1 Pro, рейтинг незавершённых набросков по Elo ведёт Gemini 3.0 Flash, а подцели уходят в AlphaProof как инструмент доказательства.
Не хотите разбираться сами? Внедряем ИИ в ваш бизнес: задачи без лимита, одна цена в месяц, отмена в любой момент.
Как проверить. Установите Lean 4 по quickstart, затем в клоне репозитория google-deepmind/alphaproof-nexus-results выполните lake exe cache get и lake build. На большой машине число потоков задаёт LEAN_NUM_THREADS, например 64.
Все доказательства лежат в открытом репозитории, разбитом на разделы Erdős, OEIS, Stacks Project и AI-коллаборации.
Первоисточник