El artículo «Advancing mathematics research with AI-driven formal proof search» presenta AlphaProof Nexus, un sistema diseñado por Google DeepMind para la investigación matemática avanzada. Los modelos de lenguaje actuales fallan por falta de fiabilidad. Esta propuesta soluciona el problema integrando inteligencia artificial con Lean, un lenguaje que verifica automáticamente cada paso lógico de una prueba.

El sistema evaluó cientos de problemas abiertos y conjeturas de gran complejidad. Logró resolver autónomamente nueve desafíos propuestos por Paul Erdős, incluyendo dos con más de cinco décadas de antigüedad. La arquitectura evolutiva del agente permite optimizar las búsquedas y reducir los costes de inferencia significativamente.

Los hallazgos demuestran la utilidad de los bucles de agentes inteligentes en la ciencia. AlphaProof Nexus ya asiste en investigaciones sobre teoría de grafos y óptica cuántica. El éxito de este método abre la puerta a una asociación profunda entre matemáticos y herramientas de verificación automática de última generación.