IA china resuelve un problema matemático abierto desde 2014 en solo 80 hora

Una IA china resuelve un problema matemático abierto desde 2014 en solo 80 horas

15 de abril de 2026 — Investigadores de la Universidad de Pekín han anunciado un hito histórico en el campo de la inteligencia artificial simbólica y el razonamiento matemático. Un sistema de IA basado en la arquitectura Rethlas ha logrado resolver una conjetura de álgebra conmutativa que permanecía sin solución desde hace 12 años, verificando además su propio resultado de forma autónoma.

El avance: De la teoría a la verificación formal

El problema, propuesto originalmente en 2014 por el matemático estadounidense Dan Anderson, se centraba en los anillos locales noetherianos cuasi-completos. Lo que hace que este logro sea excepcional no es solo el hallazgo de la solución (un contraejemplo que refuta la premisa original), sino la metodología empleada:

• Sin intervención humana: La IA procesó décadas de literatura matemática y construyó la demostración sin juicio matemático externo. El único apoyo humano fue facilitar el acceso a documentos académicos con muros de pago.

• Velocidad de ejecución: El sistema formalizó la prueba completa en 80 horas de tiempo de ejecución, una tarea que normalmente requeriría meses o años de colaboración entre expertos humanos.

• Código verificable: La solución generó aproximadamente 19,000 líneas de código en Lean 4, un lenguaje de programación y demostrador de teoremas que permite la verificación por máquina, eliminando cualquier margen de error humano.

¿Cómo funciona Rethlas?

El sistema utiliza un marco de trabajo de "agente dual" que combina dos tipos de inteligencia:

1. Razonamiento en lenguaje natural: Explora estrategias y "piensa" de forma similar a un matemático humano.

2. Verificación formal: Utiliza el motor de búsqueda de teoremas Matlas para traducir esos razonamientos en pruebas matemáticas estrictas y verificables.

Impacto en la comunidad científica

Este avance marca el paso definitivo de las IAs que resuelven problemas de olimpiadas matemáticas a sistemas capaces de abordar investigación de frontera. Según los investigadores liderados por el matemático Dong Bin, este modelo demuestra que la investigación matemática puede automatizarse sustancialmente, liberando a los científicos de tareas repetitivas y garantizando una precisión absoluta en las demostraciones.

Fuentes: MIT Technology Review, South China Morning Post, arXiv.org (Universidad de Pekín), Xataka, The Verge.