Publicado en Science el 8 de octubre de 2026, un artículo sobre AlphaProof Nexus informa que el sistema resolvió 9 de 353 problemas abiertos de Erdős y probó 44 de 492 conjeturas abiertas de la Online Encyclopedia of Integer Sequences (OEIS).
Qué resultados presenta el artículo
Dos de los problemas de Erdős resueltos llevaban 56 años abiertos. El artículo también describe resultados en dos colecciones distintas: los problemas de Erdős y las conjeturas de OEIS.
Cómo combina generación de pruebas y Lean
AlphaProof Nexus alterna la generación de pruebas matemáticas mediante un modelo de lenguaje grande (LLM) con la verificación formal en Lean, un asistente de pruebas cuyo compilador comprueba los pasos formales. Un agente básico que alternaba esas mismas etapas también reprodujo los nueve resultados de Erdős.
Qué mide cada resultado
Los denominadores corresponden a conjuntos distintos: problemas abiertos de Erdős y conjeturas abiertas de OEIS. Cada cifra se refiere a la evaluación de su propia colección.
