El 24 de mayo, Google DeepMind publicó un artículo en el que describía un bucle de agentes llamado LLM-Lean que resolvió de forma autónoma 9 de los 353 problemas abiertos propuestos por Erdős — algunos sin solución durante más de 50 años — y demostró 44 de las 492 conjeturas abiertas registradas en la OEIS, todo ello a un coste de apenas unos cientos de dólares por problema. El sistema, detallado en [2605.22763] Advancing Mathematics Research with AI-Driven Formal Proof Search, combina un modelo de lenguaje grande para generar demostraciones con el compilador de verificación formal Lean, el cual comprueba mecánicamente cada paso lógico; solo tras obtener la confirmación de corrección por parte de Lean se procede a una revisión humana. Este agente también resolvió una cuestión pendiente desde hace 15 años en el ámbito de la geometría algebraica y descubrió un nuevo parámetro algorítmico en la teoría de optimización.
Un hallazgo clave del estudio: un agente sencillo que alternaba la generación mediante el modelo de lenguaje con la retroalimentación del compilador logró replicar los 9 éxitos relacionados con Erdős; el sistema completo, que incorpora búsqueda evolutiva y aprendizaje por refuerzo, solo superó a este en los problemas más difíciles, lo cual sugiere que mejorar los modelos base podría ser más importante que aumentar la complejidad arquitectónica. El análisis de los fracasos reveló que la IA tendía a inventar lemas y a disfrazar dificultades centrales al reformularlas como lemas auxiliares; el compilador de Lean detectó automáticamente dichos errores, algo que no habrían logrado métodos de demostración informales. Actualmente, los éxitos se concentran en combinatoria, teoría de números y optimización, áreas donde la biblioteca matemática de Lean (Mathlib) está más desarrollada; los problemas que requieren crear nuevas teorías siguen fuera del alcance de este sistema.
Gary Marcus destacó que este enfoque es neurosimbólico y lo calificó de «más meticuloso y cuantitativo» que el trabajo de demostraciones informales realizado por OpenAI, lo que plantea la duda de si OpenAI precipitó su propio anuncio sabiendo que se avecinaban los resultados de DeepMind. Nate Soares señaló que los medios convencionales prácticamente ignoraron esta historia pese a su magnitud, atribuyéndolo a un «andar sonámbulo» de la sociedad hacia la inteligencia artificial transformadora. La publicación alcanzó 2,6 millones de visualizaciones en tan solo 24 horas.