El equipo de Xu Disheng, profesor visitante del Laboratorio de Inteligencia Artificial de Shanghái (Laboratorio de IA de Shanghái) y profesor de la Universidad del Área de la Gran Bahía, basándose en el gran modelo multimodal científico Intern-S2 (Shusheng-S2) y siguiendo la vía técnica de "fusión de lo general y lo especializado", completó mediante colaboración humano-máquina la demostración de la conjetura tridimensional de Ghys. El equipo del profesor Dong Bin y del académico Liu Ruochuan de la Universidad de Pekín utilizó el marco SHEAF que ellos desarrollaron para realizar la verificación formal de esta demostración, confirmando la corrección de este trabajo. Según expertos del sector, esto marca la primera vez que científicos chinos resuelven un problema matemático de nivel mundial utilizando un gran modelo chino.
La "conjetura de Ghys", propuesta en 1995 por el matemático francés Étienne Ghys, conjetura que todo sistema de Anosov holomorfo sobre una variedad compleja compacta es biholomorfamente conjugado a un automorfismo afín holomorfo de alguna variedad compleja de infra-nilpotente. Este problema combina dificultad teórica con un valor emblemático para la disciplina, y es reconocido por los expertos matemáticos en sistemas dinámicos como uno de los problemas abiertos a largo plazo más importantes del campo, una piedra de toque para poner a prueba la capacidad de razonamiento matemático.
El artículo correspondiente ya se ha publicado en la plataforma de prepublicaciones (arXiv) y su código formalizado también se ha hecho público en la plataforma Github.
La conjetura de Ghys: en busca del "código subyacente" de los sistemas caóticos
En 1995, el matemático francés Étienne Ghys planteó la conjetura de Ghys, cuya idea central es: si la existencia del comportamiento de sistemas dinámicos caóticos puede determinar una clasificación geométrica.
Este es un problema importante en el campo de los sistemas dinámicos complejos. Si esta conjetura se demuestra cierta, el problema de las trayectorias dinámicas caóticas podría "reducirse" a modelos algebraicos estándar, concisos y ordenados.
¿Cómo entender la conjetura de Ghys? Se puede imaginar un "mundo" cerrado y finito, sin frontera, en el que cada pequeña parte obedece las reglas de cálculo de los números complejos.
Para los sistemas de Anosov, se puede recurrir a la analogía del amasado: al presionar, estirar y plegar la masa, algunas direcciones se estiran y otras se comprimen. El efecto de estiramiento hace que los puntos inicialmente cercanos se separen rápidamente —una pequeña diferencia en las condiciones iniciales conduce a resultados de evolución completamente distintos.
La conjetura de Ghys dice que, si existe un movimiento tan "a la vez como amasar masa y completamente regular", entonces ese "mundo" solo puede ser una forma sumamente regular, construida por reglas simples que se repiten y ensamblan, como una retícula cristalina. Por ejemplo, el toro complejo:
Visto desde otra perspectiva, este movimiento es esencialmente una simple traslación, rotación o escalado de este "mundo". Es decir, la forma del movimiento es tan caótica que, a su vez, determina qué forma puede adoptar el mundo. El profesor Xie Junyi, del Beijing International Center for Mathematical Research de la Universidad de Pekín y ponente de 45 minutos en el Congreso Internacional de Matemáticos de 2026, comentó: "La dificultad de la conjetura de Ghys radica en que la afirmación análoga correspondiente en la versión real (numérica) sigue siendo un célebre problema completamente abierto; en el caso complejo el problema se vuelve más rígido y constituye una cuestión importante en el estudio del fenómeno de rigidez en los sistemas dinámicos complejos, extremadamente difícil".
El profesor Xu Disheng de la Universidad del Área de la Gran Bahía ha dedicado mucho tiempo a la investigación de esta conjetura; anteriormente colaboró con su director de tesis, el profesor Avila, ganador de la Medalla Fields, en el estudio del caso tridimensional, sin llegar a formular una estrategia de demostración efectiva; posteriormente, junto con su estudiante, el doctor Zhang Jiesong, obtuvo algunos resultados parcialmente relacionados con la versión débil de la conjetura de Ghys en el caso tridimensional, y dichos resultados fueron publicados en la revista matemática de primer nivel Journal of the European Mathematical Society (JEMS).
7 tandas de deducciones encadenadas y 389 nodos: la colaboración humano-máquina logra un avance clave
«El descubrimiento científico es la prueba definitiva de la inteligencia». Zhou Bowen, director y científico principal del Laboratorio de Inteligencia Artificial de Shanghái, emitió un juicio: cuanto más antiguo y fundamental es un problema, mayor es el margen de mejora de la IA. Los anticuerpos monoclonales en los que la IA participó en la investigación, el plegamiento de proteínas y las ecuaciones de Navier-Stokes, problema del milenio aún sin resolver, se ajustan a esta regla. La conjetura de Ghys en tres dimensiones es precisamente uno de estos problemas fundamentales.
En marzo de 2026, el profesor Xu Disheng se convirtió en investigador visitante del Laboratorio de IA de Shanghái, y su colaboración científica con el laboratorio entró así en una etapa más profunda y estrecha: ambas partes formaron un equipo conjunto y construyeron simultáneamente un sistema Harness orientado a escenarios de investigación matemática. El profesor Xu Disheng, con su experiencia en investigación matemática, señaló con precisión las carencias del modelo y del sistema; y, apoyándose en problemas reales de investigación matemática de frontera, impulsó múltiples rondas de iteración y refinamiento del sistema.
En agosto, el modelo Intern-S2 y su sistema asociado, ya maduro tras la iteración interna, disponía de capacidad de razonamiento recursivo a gran escala, junto con una gran flexibilidad en la interacción humano-máquina, logrando un salto cualitativo en el procesamiento de problemas matemáticos complejos. En concreto, en su primer razonamiento sobre la conjetura de Ghys en tres dimensiones, Intern-S2 produjo un informe de deducción de 400 páginas.
En cuanto a la estrategia de entrenamiento, el equipo de investigación mantuvo la línea tecnológica de «fusión de lo general y lo específico»: sobre la base de un preentrenamiento con conocimiento científico a gran escala que consolidó los cimientos del modelo, se construyeron cuidadosamente datos de postentrenamiento de nivel investigador, incluidos problemas difíciles procedentes a gran escala de artículos matemáticos y esquemas de verificación fiables, para mejorar la profesionalidad, el rigor y la normatividad del modelo en matemáticas de nivel investigador.
En cuanto a los algoritmos de entrenamiento, el equipo de investigación logró un método de entrenamiento de aprendizaje por refuerzo asíncrono para razonamientos de largo alcance, resolviendo bajo recompensas verificables una serie de problemas fundamentales como la acumulación exponencial de errores, el mantenimiento del estado a largo plazo y la autocorrección. El equipo desarrolló además un algoritmo de autoevolución que destila de forma inversa al modelo las mejoras de capacidad aportadas por el Harness, obteniendo de manera sostenida señales de supervisión eficaces en numerosos problemas de alta dificultad que superan los límites de la capacidad de deducción directa del modelo, impulsando así la mejora autónoma de sus capacidades.
En los benchmarks de matemáticas de competición y matemáticas superiores que enfatizan el razonamiento riguroso de largo alcance, como IMO-Proof y AdvancedMathBench, Intern-S2 lidera en conjunto a los modelos de código abierto existentes y supera en algunas métricas a modelos cerrados de élite como Gemini 3.1 Pro, situándose entre los modelos de código abierto con mayor capacidad de razonamiento de largo alcance del mundo.
Con esto, las capacidades del modelo base de Intern-S2 ya alcanzaban el nivel básico necesario para asistir a equipos de investigación en la resolución de problemas matemáticos de nivel investigador, pero para resolver de verdad un problema de talla mundial hacía falta subir un escalón más. El equipo consideró que la clave del avance estaba en una colaboración humano-máquina más estrecha:
Intern-S2 y su sistema asociado aprovechan la ventaja de las deducciones encadenadas a gran escala: despliegan múltiples líneas paralelas de intentos simultáneos, descomponen problemas complejos, conjeturan distintos enfoques y asumen el ingente y laborioso trabajo de deducción, entregando en cada iteración una enorme cantidad de resultados de intentos. Los investigadores, por su parte, se encargan de fijar la dirección general: juzgar qué enfoques merecen profundizar, qué caminos son callejones sin salida y ofrecer sugerencias intuitivas que sirvan de instrucciones para la siguiente iteración del sistema. No se trata de una deducción independiente de una sola parte, sino de una colaboración humano-máquina que itera mediante múltiples rondas de diálogo y retroalimentación, en una interacción estrecha.
La figura muestra el proceso de interacción en múltiples rondas del sistema y la estructura de resolución recursiva en cada ronda. Las aristas solo representan relaciones de descomposición entre subproblemas, no relaciones de dependencia de contexto; cada nodo puede acceder a todo el contexto global anterior en el tiempo a dicho nodo.
Sobre la base de la primera ronda de exploración aportada por la IA, los matemáticos Xu Disheng y Zhang Jiesong captaron con agudeza el punto de ruptura clave, retroalimentando de forma continuada al modelo y calibrando la dirección de la exploración, guiándolo hacia enfoques valiosos. Durante el proceso de investigación, Intern-S2 completó sucesivamente 7 tandas de deducciones encadenadas; el grafo del problema se expandió de 15 nodos a 389, con una producción total que alcanzó más de mil páginas de deducciones rigurosas, generando además decenas de líneas de argumentación totalmente nuevas, ayudando con éxito al equipo a resolver este problema matemático de talla mundial, y mereciendo de los académicos internacionales de frontera en este campo la valoración de que «la profundidad de pensamiento supera con mucho lo esperado».
Lo interesante es que, antes de que el artículo se subiera al sitio de prepublicaciones arXiv, el experto en sistemas dinámicos antes mencionado, el profesor Xie Junyi, también había intentado abordar el problema con GPT-6, sin encontrar un esquema de demostración. «Esto no solo confirma el valor singular de Intern-S2 en esta exploración de matemáticas de frontera, sino que transmite una señal: los grandes modelos de China también son capaces de subirse al terreno de juego de las matemáticas de frontera y contribuir a la resolución de problemas de talla mundial.»
El equipo de la Universidad de Pekín realiza una verificación formal profesional
¿Resistirán la verificación los resultados obtenidos con ayuda de la IA?
El equipo del profesor Dong Bin y del académico Liu Ruochuan de la Universidad de Pekín completó la verificación formal de los cuatro teoremas principales del artículo, y las demostraciones han pasado la comprobación de Lean. Lean, como sistema interactivo de demostración de teoremas, puede realizar verificaciones lógicas rigurosas de las demostraciones formalizadas. Los miembros clave del equipo de la Universidad de Pekín, Jiang Jiedong y Wu Bin, explicaron que todo el proceso tomó solo unos 5 días, con un pico de paralelismo de 100 agentes y una producción de unas 550.000 líneas de código Lean, mostrando una enorme escala de paralelización y una velocidad de verificación extremadamente rápida. Los expertos confirmaron que las declaraciones formales eran semánticamente consistentes con los teoremas principales del artículo, y la verificación de Lean garantiza así su corrección rigurosa.
La dificultad de la formalización proviene primero de las matemáticas mismas: las demostraciones en lenguaje natural suelen depender de que el lector complete condiciones y razonamientos con su conocimiento matemático, mientras que la formalización debe convertirlas en demostraciones completas verificables por computadora. Si los resultados citados por el artículo no están en la biblioteca de teoremas básicos, es necesario añadir demostraciones formales o buscar rutas alternativas que aprovechen resultados existentes. En particular, el campo de los sistemas dinámicos carecía de infraestructura formal suficiente; este trabajo añadió gran cantidad de infraestructura, cubriendo los numerosos resultados de la literatura de los que depende el artículo. Para las matemáticas de nivel investigador, estos trabajos implican la expresión precisa de definiciones, la descomposición de la estructura de las demostraciones y la elección de herramientas matemáticas; cuando muchos agentes trabajan en paralelo, además, hay que asegurar que las definiciones, declaraciones y dependencias de las distintas partes se articulen entre sí, para que las demostraciones locales conformen una cadena de demostración completa.
Para organizar este proceso, el equipo de la Universidad de Pekín utilizó el framework SHEAF, desarrollado por ellos mismos: varios agentes organizan las proposiciones, definiciones y relaciones de dependencia del artículo en un grafo acíclico dirigido que se extiende por capas desde el teorema objetivo hasta la biblioteca de teoremas básicos; el modelo, bajo el framework, participa en la descomposición de proposiciones y la construcción de demostraciones formales, y el equipo organiza el trabajo en torno a ese grafo, siguiendo el estado de declaración, demostración y poda de cada nodo, descomponiendo la tarea de formalización a gran escala en pasos articulados y verificables.
Ya en 2021, cuando los grandes modelos aún no habían aparecido, el equipo del profesor Dong Bin del Centro de Matemáticas Internacionales de Pekín (BICMR) de la Universidad de Pekín percibió con agudeza que la inteligencia artificial transformaría el paradigma de la investigación matemática. El equipo de matemáticas de la Universidad de Pekín es uno de los primeros del mundo en orientarse hacia AI for Math, y ha construido una cadena tecnológica completa que abarca conjuntos de evaluación de alta dificultad (FATE), recuperación de conocimiento matemático a gran escala (Matlas/LeanSearch) y razonamiento automático y verificación formal (Rethlas/Archon/Danus/Iteris); su sistema de IA resolvió con éxito la conjetura de Anderson, un problema matemático abierto, logrando el primer caso nacional y, a la vez, el primer resultado internacional liderado por un equipo universitario que resolvió de forma autónoma, mediante inteligencia artificial, una conjetura matemática de gran envergadura. Recientemente, el equipo también completó de manera independiente la verificación formal de la conjetura de Poincaré.
De la resolución de un único problema difícil a la infraestructura de investigación científica
La importancia de esta investigación también radica en que valida un nuevo paradigma de investigación científica. La investigación matemática tradicional depende del largo proceso de exploración de talento individuales excepcionales, mientras que este avance conecta sistemáticamente la intuición de los expertos con el circuito de resolución por máquina, formando un bucle cerrado de “exploración sistémica—juicio experto—acumulación de resultados—corrección mediante retroalimentación”. Este paradigma puede replicarse y extenderse a más áreas de investigación básica con “espacios de búsqueda enormes y expertos escasos”, logrando más avances de innovación original “de 0 a 1”.
A continuación, apoyándose en el bucle completo de capacidades puesto a prueba en esta investigación, el equipo lo empaquetará aún más como un módulo de verificación matemática reutilizable de la plataforma de descubrimiento científico 书生·端砚 (InternEscience), para que pueda invocarse directamente en investigaciones futuras de problemas científicos. Al mismo tiempo, tomando el avance en la conjetura de Ghys tridimensional como punto de partida, el Laboratorio de IA de Shanghái extenderá las capacidades de razonamiento acumuladas a otras disciplinas homólogas en estructura matemática; tras obtener nuevos avances, empaquetará las nuevas capacidades de razonamiento de vuelta en la plataforma 端砚 para su reutilización, combinándolas con más disciplinas en busca de la siguiente ronda de avances, formando un volante de autoevolución de “avance—empaquetado—reutilización—nuevo avance”. 雷峰网 (cuenta pública: 雷峰网) también seguirá de cerca los últimos avances en esta dirección.
Artículo original de 雷峰网, prohibida su reproducción sin autorización. Para más detalles, véaseAviso de reproducción。