🧠 В исследовании Google DeepMind агент формального поиска доказательств решил 9 из 353 открытых задач Эрдёша и доказал 44 из 492 гипотез OEIS, базы целочисленных последовательностей.

Заявленные вычислительные затраты на решённую задачу Эрдёша составили несколько сотен долларов.

Модель предлагает доказательство на языке Lean, получает результат проверки и продолжает поиск с учётом ошибок. Убедительно написанного текста недостаточно: формальный проверяющий должен принять доказательство.

Даже более простой агент, чередующий генерацию и проверку, повторил успехи на задачах Эрдёша. Но на самых сложных задачах оказался дороже. Значение имеет и организация поиска.

https://www.thedailystar.net/news/technology/news/ai-can-now-solve-complex-mathematical-research-problems-scientists-say-4296911

https://arxiv.org/abs/2605.22763