DeepMind acopló modelos de lenguaje a Lean y a geometría sintética para resolver problemas olímpicos con pruebas chequeables.
AlphaGeometry abordó geometría con generación de construcciones auxiliares; AlphaProof reforzó demostración en Lean vía RL y autoformalización.
El combo mostró un template exportable: conjeturar en lenguaje natural, formalizar, buscar, verificar.
Ese template es el puente conceptual hacia esfuerzos posteriores en análisis y EDPs con asistencia masiva de agentes.
Asistentes de prueba basados en LLM aceleraron bibliotecas Lean; matemáticos adoptaron flujos híbridos humano–máquina.
La revista Science publicó el 8 de octubre de 2026 el artículo de Google DeepMind sobre AlphaProof Nexus, un marco de agentes que genera demostraciones formales verificadas en Lean y que resolvió 9 de 353 problemas de Erdős intentados y 44 de 492 conjeturas abiertas de la OEIS.
Sistemas de DeepMind y OpenAI alcanzaron desempeños nivel medalla en IMO con pipelines de búsqueda y formalización.