AlphaProof Nexus от Google DeepMind решил 9 из 353 открытых задач Эрдёша — включая две, над которыми математики бились 56 лет. На каждую задачу ушло всего несколько сотен долларов вычислений. Как это работает. Агент использует Lean — язык формальных доказательств с машинной проверкой. Координирует поиск эволюционный алгоритм: перебирает варианты доказательств, отбрасывает тупики, наращивает успешные ветки. Это не генерация убедительного текста, а логически верифицируемый результат. Замеры. Параллельно агент доказал 44 гипотезы из 492 из базы OEIS — набор целочисленных последовательностей. Успехи сконцентрированы в областях с развитой формализованной библиотекой, где доказательства разбиваются на подзадачи. Всё упирается в формализацию: задачи, требующие построения новой теории, остаются за гранью. Какие именно задачи Эрдёша решены и подтверждены ли они сообществом — неизвестно. Что это значит: формальные языки доказательств превращают языковую модель в инструмент, способный закрывать реальные математические гипотезы, а не только олимпиадные задачи.