Исследование AlphaProof Nexus опубликовано в Science после рецензирования

Система Google DeepMind решила девять из 353 открытых задач Эрдёша и доказала 44 из 492 гипотез энциклопедии целочисленных последовательностей OEIS. Сгенерированные доказательства записывались на формальном языке Lean и автоматически проверялись его компилятором.

Рецензируемый журнал Science опубликовал исследование Google DeepMind о системе AlphaProof Nexus для автоматического поиска формальных математических доказательств.

AlphaProof Nexus использует агентов на основе больших языковых моделей, которые создают и исправляют доказательства с учётом сообщений компилятора Lean. Формальная проверка каждого шага позволяет отсеивать логические ошибки и вымышленные утверждения, характерные для генеративных моделей.

Система решила девять из 353 открытых задач Эрдёша и доказала 44 из 492 открытых гипотез из базы On-Line Encyclopedia of Integer Sequences (OEIS). Авторы также применяли её в исследованиях по комбинаторике, оптимизации, теории графов, алгебраической геометрии и квантовой оптике.

Препринт исследования был опубликован в мае 2026 года. Сгенерированные доказательства на Lean и их текстовые версии доступны в репозитории Google DeepMind и могут быть повторно проверены с помощью Lean 4.