Un problema matemático de 1995 alcanza un nuevo hito
Una conjetura matemática planteada en 1995 ha dado lugar a una demostración que abarca la dimensión compleja tres, gracias a la colaboración entre matemáticos y el modelo Intern-S2 del Laboratorio de Inteligencia Artificial de Shanghái. Posteriormente, un equipo de la Universidad de Pekín tradujo los cuatro teoremas principales del artículo en demostraciones verificadas por Lean, un sistema informático diseñado para comprobar el razonamiento matemático.
Contenido
- Un problema matemático de 1995 alcanza un nuevo hito
- Qué dice la demostración sobre el movimiento y la forma
- Por qué importa el alcance preciso
- De una prueba de olimpiada a una colaboración de investigación
- Cómo guiaron los matemáticos a la inteligencia artificial
- Qué aportó el software de apoyo
- Cómo verificó la demostración la Universidad de Pekín
- Por qué las dos etapas se complementan
- El siguiente paso: un módulo de verificación reutilizable
- Puntos clave
El Laboratorio de Inteligencia Artificial de Shanghái anunció el logro el 15 de octubre de 2026 y atribuyó el trabajo a un equipo dirigido por Disheng Xu, profesor de la Universidad de Great Bay e investigador visitante del laboratorio. El artículo de investigación, «Difeomorfismos holomorfos de Anosov de codimensión uno», señala como único autor a Jiesong Zhang, del Real Instituto de Tecnología KTH de Suecia.
El resultado resuelve el caso de codimensión uno de la conjetura del matemático francés Etienne Ghys, incluido el caso de dimensión compleja tres. La cuestión aborda una relación llamativa entre movimiento y forma: si un espacio que admite un tipo particular de movimiento caótico debe tener, en sí mismo, una estructura matemática muy ordenada.
Intern-S2 contribuyó al desarrollo de ideas y argumentos mediante intercambios reiterados con los investigadores. Zhang afirma en su declaración sobre el uso de inteligencia artificial que verificó por su cuenta todas las matemáticas. La colaboración combinó exploración con máquinas, criterio humano y un proceso independiente de verificación formal.
El laboratorio describe el logro como la primera ocasión en que un modelo chino de inteligencia artificial ayuda a resolver un problema matemático de esta importancia. El resultado concreto es un teorema de clasificación, acompañado de una prepublicación de acceso público y código de formalización publicado abiertamente.
Qué dice la demostración sobre el movimiento y la forma
La conjetura de Ghys pertenece a la dinámica compleja, que estudia cómo cambian los sistemas matemáticos cuando sus coordenadas siguen las reglas de los números complejos. Un número complejo tiene dos componentes reales, por lo que la dimensión compleja tres corresponde localmente a seis dimensiones reales. Se trata de un marco más abstracto que el de un objeto corriente que se desplaza por una habitación.
Un sistema de Anosov combina de manera precisa estiramiento y compresión. Con el movimiento repetido, algunas direcciones se contraen mientras otras se expanden. Los puntos de partida cercanos pueden separarse rápidamente, lo que produce un comportamiento caótico aunque la regla que rige cada paso sea exacta.
Una imagen útil es la de un proceso repetido que estira y pliega una forma. El sistema matemático estudiado aquí es mucho más restrictivo: el estiramiento y la contracción deben cumplir condiciones uniformes, y el movimiento debe preservar la estructura que aportan las coordenadas complejas.
Ghys planteó que esos sistemas, en variedades complejas compactas, deberían tener una descripción algebraica estándar. Una variedad es un espacio que parece sencillo en un entorno pequeño, aunque su forma completa sea complicada. En este contexto, la compacidad es una condición matemática que impide que el espacio se extienda indefinidamente.
El teorema de Zhang afirma que todo difeomorfismo holomorfo de Anosov de codimensión uno en una variedad compleja compacta y conexa es biholomórficamente conjugado a un automorfismo hiperbólico de un toro complejo. En términos más sencillos, un cambio reversible de coordenadas que respeta la estructura compleja transforma el movimiento en una transformación algebraica estándar en un espacio muy regular.
Un toro complejo puede construirse identificando puntos del espacio complejo que difieren en elementos de una red periódica. El logro central consiste en demostrar que la dinámica compleja obliga a adoptar esta descripción geométrica ordenada.
Por qué importa el alcance preciso
El artículo aborda el caso de codimensión uno. En estos sistemas, esto significa que una de las partes contractivas o expansivas tiene dimensión compleja uno. El teorema abarca en general esta familia restringida y resuelve la conjetura en dimensión compleja tres.
La conjetura más amplia de Ghys trata sobre sistemas holomorfos de Anosov en una gama más extensa de variedades complejas y los describe mediante modelos algebraicos estándar en espacios llamados variedades infra-nil complejas. El resultado de Zhang ofrece una respuesta particularmente rígida para el caso estudiado: un toro complejo y un automorfismo hiperbólico.
Para los matemáticos que trabajan en este caso, el teorema cambia el problema: en lugar de identificar un espacio y un movimiento desconocidos, permite estudiar un modelo estándar. Un cambio de coordenadas vincula el sistema original con ese modelo y preserva la geometría compleja.
Xu llevaba años estudiando el problema. Antes había investigado el caso de dimensión tres con su antiguo asesor, Artur Avila, ganador de la Medalla Fields. Más adelante, Xu y Zhang obtuvieron resultados parciales relacionados, publicados en el Journal of the European Mathematical Society. El nuevo trabajo se basa en esa atención sostenida a la misma cuestión matemática.
De una prueba de olimpiada a una colaboración de investigación
La participación de Intern-S2 se produjo después de un resultado anterior de Intern-S1 en la Olimpiada Matemática China de 2025. Ese año, el comité de la Sociedad Matemática China responsable de las competiciones de matemáticas de secundaria organizó una prueba de inteligencia artificial e invitó a tres modelos chinos a resolver problemas en el mismo tiempo que los participantes humanos.
Intern-S1 obtuvo 102 puntos con los mismos criterios de calificación y quedó en primer lugar entre los tres modelos participantes. El umbral para la medalla de oro era de 78 puntos, por lo que su resultado lo superó en 24 puntos, alrededor de un 31 %.
Xu vio potencial para utilizar esta familia de modelos en la investigación matemática, mientras que el Laboratorio de Inteligencia Artificial de Shanghái quería pasar de los problemas de competición a las preguntas aún sin resolver. La colaboración comenzó a principios de 2026 e incluyó el desarrollo de un sistema de software, descrito como un «Harness», para organizar el trabajo del modelo y sus intercambios con los investigadores.
Las principales etapas fueron:
- 1995: Etienne Ghys plantea la conjetura.
- 2025: Intern-S1 obtiene 102 puntos en la prueba de inteligencia artificial de la Olimpiada Matemática China.
- Principios de 2026: Xu y el Laboratorio de Inteligencia Artificial de Shanghái comienzan su colaboración para entrenar el modelo.
- Marzo de 2026: Xu se convierte en investigador visitante del laboratorio.
- Agosto de 2026: Una versión desarrollada internamente de Intern-S2 y su sistema de apoyo alcanzan la etapa utilizada para la exploración matemática intensiva.
- 29 de septiembre: El artículo de Zhang se publica en arXiv; el 13 de octubre se publica una revisión.
- 15 de octubre de 2026: Se anuncia públicamente el logro.
Cómo guiaron los matemáticos a la inteligencia artificial
La primera exploración del problema por parte de Intern-S2 produjo un informe de derivaciones de unas 400 páginas. Xu invitó a Zhang, antiguo alumno suyo e investigador posdoctoral en KTH, a sumarse al trabajo como investigador visitante. Zhang seguía la conjetura de Ghys desde sus estudios doctorales.
Xu y Zhang examinaron las propuestas del modelo, identificaron vías prometedoras y aportaron comentarios para orientar las exploraciones posteriores. La máquina siguió distintas líneas de razonamiento y generó argumentos; los matemáticos decidieron qué caminos merecían más trabajo y ayudaron a elaborar la demostración final.
El laboratorio describe siete rondas de razonamiento continuado. Durante el proceso, el grafo de problemas del modelo pasó de 15 a 389 nodos, mientras que la producción acumulada llegó a unas mil páginas e incluyó decenas de enfoques propuestos.
Un grafo de problemas es un mapa de tareas matemáticas más pequeñas y de las conexiones entre ellas. Un nodo puede representar una afirmación intermedia, mientras que otro representa un resultado necesario para demostrarla. El aumento registrado muestra hasta qué punto el sistema dividió y exploró el problema.
La declaración de Zhang sobre el uso de inteligencia artificial explica directamente quién responde por las matemáticas finales: una versión interna de Intern-S2 ayudó a desarrollar ideas y argumentos en varias rondas de diálogo, y él verificó por su cuenta las matemáticas. En su artículo también agradece a Xu las conversaciones continuadas.
Qué aportó el software de apoyo
El Laboratorio de Inteligencia Artificial de Shanghái combinó el modelo con un software concebido para gestionar largas cadenas de razonamiento y comentarios humanos reiterados. El sistema podía dividir una pregunta difícil en tareas más pequeñas, explorar varias vías y devolver resultados para que los investigadores los evaluaran.
El enfoque de entrenamiento combinó conocimientos científicos amplios con material orientado a las matemáticas de investigación, incluidos problemas difíciles extraídos de artículos matemáticos y métodos para comprobar las soluciones propuestas. El laboratorio también describe el uso de aprendizaje por refuerzo con recompensas verificables: un razonamiento correcto y comprobable podía servir como señal de entrenamiento.
Después, los investigadores utilizaron la experiencia obtenida con el sistema de apoyo para mejorar el propio modelo. El objetivo práctico era mantener avances útiles a lo largo de una investigación prolongada, entre otras cosas mediante el seguimiento de resultados intermedios y la corrección de errores a medida que se desarrollaban nuevos argumentos.
El laboratorio también citó resultados en IMO-Proof y AdvancedMathBench, evaluaciones centradas en el razonamiento matemático. En el proyecto sobre la conjetura de Ghys, las pruebas más detalladas del funcionamiento del sistema son la sucesión de extensas derivaciones, los comentarios de expertos, el artículo terminado y la posterior verificación formal.
Cómo verificó la demostración la Universidad de Pekín
El equipo de la Universidad de Pekín, dirigido por Bin Dong y Ruochuan Liu, utilizó su marco SHEAF para formalizar los cuatro teoremas principales del artículo de Zhang. El trabajo también abarcó resultados de Ghys de los que dependen los argumentos.
La formalización traduce definiciones, supuestos y razonamientos matemáticos a un lenguaje que un ordenador puede verificar. Un artículo convencional puede confiar en que un lector con formación complete los pasos conocidos. Lean exige expresar esos pasos mediante enunciados precisos y operaciones lógicas permitidas.
Los integrantes del equipo Jiedong Jiang y Bin Wu dijeron que el trabajo tomó unos cinco días y que llegaron a funcionar en paralelo hasta 100 agentes de inteligencia artificial. El resultado fue de aproximadamente 550.000 líneas de código Lean. Los expertos también comprobaron que los enunciados formales coincidieran con el significado matemático de los teoremas principales del artículo.
SHEAF organizó la tarea como un grafo dirigido de definiciones, proposiciones y dependencias. Esto permitió que distintos agentes trabajaran en partes relacionadas mientras el equipo hacía un seguimiento de qué enunciados ya tenían demostración y cuáles aún requerían trabajo.
La formalización exigió algo más que traducir los argumentos finales. Faltaban en las bibliotecas de matemáticas formalizadas existentes algunos resultados de apoyo sobre dinámica. El equipo tuvo que aportar esos fundamentos o encontrar vías que utilizaran resultados ya disponibles y, después, conectar las distintas partes en una cadena completa.
El artículo está disponible como prepublicación en arXiv, y el código de formalización se ha publicado en GitHub. El anuncio no especificó si se había enviado a una revista ni si había pasado por una revisión por pares.
Por qué las dos etapas se complementan
Intern-S2 y SHEAF cumplieron funciones diferentes. El primero ayudó a buscar ideas y argumentos matemáticos. El segundo contribuyó a construir demostraciones formales que Lean pudiera verificar. Los matemáticos guiaron la exploración, comprobaron las matemáticas resultantes y evaluaron si los enunciados formales reflejaban los teoremas que se pretendía demostrar.
La escala del trabajo muestra con claridad esa división. Unas mil páginas de resultados exploratorios dieron paso a un artículo de investigación; el proceso de verificación generó después unas 550.000 líneas de código formal. Cada etapa convirtió el trabajo en un formato distinto, adecuado para una tarea diferente.
Para los investigadores futuros, el artículo público presenta el argumento matemático, mientras que el código público registra la estructura de la demostración formal. Las definiciones y los resultados de apoyo incorporados durante la formalización también pueden servir de punto de partida para investigaciones posteriores en el mismo campo.
El siguiente paso: un módulo de verificación reutilizable
El Laboratorio de Inteligencia Artificial de Shanghái planea integrar este flujo de trabajo en un módulo de verificación matemática para su plataforma de descubrimiento científico Intern Duanyan. El objetivo es que otros proyectos puedan reutilizar la combinación de exploración con modelos, comentarios de expertos y verificación formal.
El laboratorio también tiene previsto aplicar a otras disciplinas con estructuras matemáticas relacionadas las capacidades de razonamiento desarrolladas en este proyecto. El ciclo propuesto consiste en resolver un problema de investigación, convertir los métodos útiles en software reutilizable y aplicarlos a otra investigación.
Para Xu, el resultado amplía una larga trayectoria de investigación mediante la colaboración entre la Universidad de Great Bay, el Laboratorio de Inteligencia Artificial de Shanghái, KTH y la Universidad de Pekín. Para la comunidad matemática en general, aporta tanto un nuevo resultado de clasificación como un ejemplo detallado de participación de la inteligencia artificial en una investigación bajo dirección humana.
Puntos clave
- La nueva demostración resuelve el caso de codimensión uno de la conjetura de Ghys, incluida la dimensión compleja tres.
- Jiesong Zhang es el único autor del artículo de investigación y afirma que verificó por su cuenta todas las matemáticas.
- Disheng Xu y Zhang guiaron a Intern-S2 mediante sucesivas exploraciones y comentarios.
- El grafo de problemas del modelo pasó de 15 a 389 nodos y produjo unas mil páginas de derivaciones.
- El marco SHEAF de la Universidad de Pekín ayudó a formalizar en Lean cuatro teoremas principales y resultados de apoyo.
- El proceso de verificación tomó, según se informó, unos cinco días y generó aproximadamente 550.000 líneas de código.
- El laboratorio planea convertir el flujo de trabajo en un módulo de verificación matemática reutilizable.
