Una IA china resuelve un problema matemático planteado hace una década

La inteligencia artificial sigue ampliando su terreno de juego, y esta vez lo ha hecho en un campo especialmente difícil: las matemáticas de nivel investigador. Un equipo de la Universidad de Pekín asegura haber desarrollado un sistema capaz de resolver de forma autónoma un problema abierto de álgebra con diez años de antigüedad, formulado en 2014 por el matemático estadounidense Dan Anderson, antiguo profesor de la Universidad de Iowa y fallecido en 2022.

Lo más llamativo no es solo que la IA haya encontrado una solución, sino que también habría sido capaz de verificar formalmente su propia demostración sin intervención humana significativa. El trabajo ha sido publicado en arXiv, por lo que todavía no ha sido revisado por pares, pero plantea una idea muy potente: que la investigación matemática podría automatizarse en mucha mayor medida de lo que se pensaba hasta ahora.

Una IA entrenada para investigar matemáticas avanzadas

Según explican los investigadores, liderados por el matemático Dong Bin, el sistema fue diseñado para enfrentarse a problemas matemáticos de nivel avanzado combinando dos capacidades que normalmente no conviven bien en los modelos de IA actuales: por un lado, el razonamiento en lenguaje natural y, por otro, la verificación formal rigurosa.

Ese punto es importante, porque en matemáticas no basta con que una solución “parezca correcta”. Una demostración tiene que ser completamente sólida. Incluso los textos escritos por expertos pueden contener errores sutiles, y en el caso de los grandes modelos de lenguaje el problema es aún mayor, ya que pueden generar respuestas convincentes pero incorrectas, algo que en IA se conoce como “alucinación”.

Precisamente por eso, el equipo chino plantea un marco de trabajo que no se limita a generar ideas, sino que también las transforma en pruebas verificables dentro de un entorno formal.

El problema de Dan Anderson que la máquina logró resolver

El estudio sostiene que el sistema consiguió resolver una conjetura de álgebra conmutativa propuesta por Dan Anderson en 2014. El texto no presenta esta hazaña como una simple asistencia al investigador humano, sino como una resolución prácticamente autónoma.

De hecho, los autores afirman que lograron resolver el problema abierto y formalizar automáticamente la prueba con esencialmente ninguna intervención humana. También subrayan que el sistema necesitó unas 80 horas de ejecución para alcanzar el resultado.

Según los investigadores, durante ese proceso no fue necesario ningún juicio matemático por parte del operador humano, lo que refuerza la idea de que la IA no solo ayudó, sino que llevó el peso real del trabajo.

Cómo funciona este sistema de IA matemática

La arquitectura presentada por el equipo combina varias herramientas especializadas. El primer componente es un sistema de razonamiento llamado Rethlas, que se apoya en un buscador de teoremas matemáticos denominado Matlas. Su función es explorar posibles estrategias de resolución siguiendo un flujo de trabajo que recuerda al que utilizan los matemáticos cuando atacan un problema abierto: revisar resultados previos, buscar conexiones útiles y plantear caminos de prueba plausibles.

Cuando Rethlas encuentra una posible demostración, entra en juego un segundo sistema llamado Archon. Esta herramienta utiliza otro motor de búsqueda, LeanSearch, para convertir la idea obtenida en un proyecto formal apto para ser procesado por un demostrador interactivo de teoremas.

Ese demostrador es Lean 4, que además de ser una herramienta para verificar pruebas matemáticas, también funciona como lenguaje de programación. Lean 4 cuenta con una biblioteca mantenida por la comunidad que reúne cientos de miles de teoremas y definiciones, algo clave para construir demostraciones complejas sin partir de cero en cada paso.

En otras palabras, el sistema no se limita a “proponer” una solución, sino que intenta expresarla en un lenguaje matemático formal que pueda comprobarse rigurosamente.

Más rápido que un humano y capaz de unir especialidades

Los investigadores aseguran que el sistema fue capaz de realizar tareas matemáticas más rápido que cualquier humano y, además, abordar de forma independiente trabajos que normalmente exigirían colaboración entre expertos de diferentes áreas.

Ese detalle resulta especialmente interesante porque una parte importante de la investigación matemática actual depende precisamente de la interacción entre especialistas con conocimientos muy distintos. Si una IA consigue enlazar herramientas, teoremas y estrategias procedentes de varios subcampos de forma autónoma, estaríamos ante un cambio importante en la manera de afrontar la investigación teórica.

Los autores del trabajo sostienen que este caso ofrece un ejemplo concreto de cómo la investigación matemática podría ser sustancialmente automatizada mediante inteligencia artificial.

Por qué las matemáticas siguen siendo un reto enorme para la IA

Aunque el anuncio suene muy llamativo, conviene ponerlo en contexto. En todo el mundo se están entrenando sistemas de IA para resolver problemas matemáticos, pero la mayoría todavía necesita una supervisión humana considerable para llegar a resultados fiables.

La razón es simple: las matemáticas exigen una precisión total. Un pequeño error lógico invalida toda la prueba, y los modelos generativos tradicionales no son especialmente buenos manteniendo esa consistencia de principio a fin. Pueden redactar explicaciones elegantes, pero eso no garantiza que la estructura lógica sea correcta.

Por eso el enfoque del equipo chino resulta especialmente relevante. En lugar de confiar únicamente en un modelo que “razone” en lenguaje natural, combinan ese razonamiento con una capa de formalización y verificación estricta, que actúa como filtro contra errores e inconsistencias.

Autonomía casi total, aunque con margen para mejorar

Aun así, los propios investigadores reconocen que la intervención de un matemático puede seguir siendo útil. En sus pruebas, observaron que el proceso podía acelerarse si un experto humano guiaba parcialmente a Archon.

Eso sugiere que, aunque el sistema puede funcionar casi en solitario, todavía hay espacio para modelos híbridos en los que el investigador humano marque dirección estratégica y la IA se encargue de una parte enorme del trabajo técnico y formal.

Lejos de vender una sustitución total e inmediata de los matemáticos, el estudio apunta más bien a una nueva dinámica de colaboración: sistemas informales y formales trabajando en paralelo para reducir de forma muy notable el esfuerzo humano necesario para producir resultados verificables.

Lo que implica este avance para el futuro de la investigación

Si estos resultados se confirman tras la revisión por pares, estaríamos ante una demostración muy seria de que la IA puede ir más allá de redactar textos, programar o resumir artículos. También podría empezar a desempeñar un papel activo en la creación de conocimiento matemático nuevo.

Eso no significa que las máquinas vayan a reemplazar mañana a los investigadores, pero sí abre la puerta a una transformación profunda. En un escenario así, los matemáticos podrían dedicar menos tiempo a la verificación tediosa, al rastreo manual de teoremas previos o a la formalización técnica, y concentrarse más en la intuición, la estrategia y la interpretación de resultados.

La clave estará en comprobar hasta qué punto este sistema puede generalizarse a otros problemas abiertos, otros campos de las matemáticas y entornos menos controlados.

Una señal de hacia dónde se dirige la IA científica

Más allá del caso concreto de la conjetura de Anderson, este trabajo refleja una tendencia cada vez más clara: la IA ya no solo quiere ayudar a buscar información o automatizar tareas rutinarias, sino entrar de lleno en disciplinas donde la exigencia intelectual es máxima.

Que una máquina pueda resolver un problema de álgebra conmutativa, apoyarse en literatura matemática acumulada durante décadas y producir una demostración formalmente verificable sin apenas ayuda humana es, como mínimo, una señal potente de hacia dónde se dirige la investigación en inteligencia artificial.

Ahora falta lo más importante: que la comunidad científica valide el trabajo, compruebe la solidez del resultado y determine si estamos ante un caso aislado o ante el primer ejemplo real de una nueva era en la investigación matemática asistida —o directamente impulsada— por IA.