Una conjetura de hace treinta años, un modelo chino y una demostración verificada por máquina

Una conjetura de hace treinta años, un modelo chino y una demostración verificada por máquina

El 15 de octubre, Shanghai AI Laboratory (上海人工智能实验室) anunció que un equipo de investigación había demostrado el caso tridimensional de la conjetura de Ghys, un problema abierto en sistemas dinámicos que sigue en pie desde 1995. El trabajo se desarrolló con Intern-S2, el modelo propio del laboratorio, y la demostración final fue verificada formalmente en Lean por un equipo de Peking University (北京大学).

La relevancia no está solo en que cayera un problema difícil. Está en que el anuncio se estructuró en torno a un proceso y no a un número: un modelo que produce derivaciones, investigadores que eligen en qué líneas de ataque invertir atención y un asistente de demostración que certifica cada paso. Esa combinación es la que la industria promete desde hace dos años, y aquí está, con un artículo adjunto.

Qué pregunta la conjetura

Étienne Ghys planteó el problema en 1995. En términos generales, pregunta si el comportamiento de los sistemas dinámicos caóticos puede determinar su clasificación geométrica, lo que equivale a preguntar si el movimiento revela la forma del espacio en el que ocurre.

Lo que se resolvió no es la pregunta general. El equipo demostró el caso de codimensión uno, es decir, el marco tridimensional, que había permanecido abierto durante tres décadas. Esa distinción importa para leer la afirmación con honestidad: la conjetura completa sigue siendo más amplia, pero el caso concreto que había resistido a todos hasta ahora queda zanjado.

La primera pasada produjo cuatrocientas páginas

La mecánica de la colaboración es más interesante que el resultado, porque muestra cómo se ve en la práctica la investigación humano-IA minuto a minuto.

La primera exploración del problema por parte de Intern-S2 produjo un informe de derivación de unas 400 páginas. Eso no es una respuesta. Es un montón de razonamiento candidato, parte útil y parte no, que es precisamente la forma de salida que se obtiene cuando se pide a un modelo que piense en algo genuinamente no resuelto en vez de recordar algo conocido.

A partir de ahí, el trabajo pasó por siete rondas de razonamiento continuado. El grafo del problema, un mapa de subafirmaciones y de cómo dependen unas de otras, creció de 15 a 389 nodos. La producción acumulada llegó a unas mil páginas e incluyó docenas de enfoques distintos. En cada etapa, los matemáticos hicieron lo que el modelo no puede hacer por sí mismo: examinaron las propuestas, decidieron qué aperturas eran prometedoras y orientaron la ronda siguiente.

Xu Disheng, investigador visitante en el laboratorio y profesor en la Greater Bay University, y Zhang Jiesong, investigador postdoctoral que ha seguido la conjetura desde sus estudios de doctorado, aportaron ese criterio. El artículo de Zhang, publicado en arXiv el 29 de septiembre y revisado el 13 de octubre, es un trabajo de autor único con una declaración de uso de IA: el modelo ayudó a desarrollar las ideas y los argumentos mediante múltiples rondas de diálogo, y él comprobó las matemáticas de forma independiente.

La parte que lo convierte en algo más que una historia

Las afirmaciones sobre que la IA resuelve matemáticas son baratas. Lo que da peso a esta es que la demostración se formalizó.

El equipo de Peking University, dirigido por Bin Dong y Ruochuan Liu, usó su propio marco SHEAF para formalizar los cuatro teoremas principales, además de los resultados de apoyo de Ghys de los que dependen los argumentos. Formalizar significa traducir las definiciones, los supuestos y el razonamiento a un lenguaje que una computadora pueda comprobar, donde cada paso del argumento del autor tiene que escribirse explícitamente en lugar de dejarse para que lo complete un lector formado.

El esfuerzo llevó unos cinco días, con hasta 100 agentes trabajando en paralelo, y produjo aproximadamente 550.000 líneas de código Lean. Lean es un demostrador de teoremas interactivo. No le importa cuán seguro se sienta alguien. Comprueba la lógica y acepta la demostración o no la acepta.

SHEAF organizó la tarea como un grafo dirigido de definiciones, proposiciones y dependencias, de modo que agentes separados pudieran trabajar en piezas conectadas mientras el equipo seguía qué afirmaciones tenían demostración y cuáles aún la necesitaban. Es un tipo de división del trabajo genuinamente nuevo, y el marco además tuvo que cubrir huecos en la biblioteca formal existente para sistemas dinámicos, porque la maquinaria que esta demostración necesitaba simplemente no existía todavía.

Humanos y modelo, tareas distintas

La división del trabajo descrita por el laboratorio merece tomarse al pie de la letra, porque no es la versión halagadora para ninguna de las partes.

El modelo peinó la literatura, descompuso la proposición en piezas, exploró ramas de demostración en paralelo, comprobó pasos lógicos y probó un gran número de ideas con rapidez. Los humanos fijaron la dirección, juzgaron qué enfoques valía la pena perseguir y tomaron las decisiones que determinaban dónde gastar el esfuerzo de la siguiente ronda.

Ninguna de las dos mitades se parece a la otra. La contribución del modelo es escala y aguante: puede sostener docenas de callejones sin salida en la mente sin desanimarse. La contribución de los humanos es el gusto, es decir, la capacidad de mirar cien páginas de razonamiento plausible y saber qué tres párrafos importan.

Hay una anécdota asociada de la que la prensa china hizo mucho. Un experto en sistemas dinámicos, según se dice, planteó el mismo problema a GPT-6 por curiosidad después de oír que un modelo nacional lo había resuelto, y no llegó. Leído en sentido estricto, es una comparación entre dos sistemas en un problema, lo que demuestra muy poco. Leído como señal sobre la dinámica competitiva, es el tipo de detalle que mueve inversiones.

Por qué la verificación formal cambia lo que está en juego

Durante la mayor parte de los últimos dos años, el cuello de botella de las matemáticas asistidas por IA no ha sido generar argumentos candidatos. Los modelos son buenos produciendo razonamiento plausible. El cuello de botella ha sido saber cuál de todo eso es correcto, porque comprobar una demostración es lento, requiere expertos y no se paraleliza bien.

Lean invierte eso. Una vez que un enunciado se formaliza, la verificación es barata y rápida, y se puede confiar en ella porque es mecánica en lugar de social. Las 550.000 líneas son la parte costosa, y que un equipo más cien agentes pudieran producirlas en cinco días es el verdadero avance aquí. Sugiere que el cuello de botella de la verificación podría estar aflojándose justo cuando el de la generación ya estaba suelto.

El laboratorio dice que empaquetará el flujo de trabajo como un módulo reutilizable de verificación matemática en su plataforma de descubrimiento científico, conectando el modelo, los agentes, los datos y el equipo experimental. También cita un resultado anterior, en el que un equipo de Wuhan University (武汉大学) usó la plataforma para reducir el ciclo de desarrollo de una síntesis electroquímica de cinco a diez años a uno o dos.

Qué sacar de todo esto

El resumen honesto es que se trata de un resultado real con una demostración real, producido por un flujo de trabajo que sigue siendo muy intensivo en personas. Siete rondas de dirección experta no son un modelo funcionando por su cuenta. Un artículo de autor único con una declaración de uso de IA no es un modelo reclamando mérito.

Lo que ha cambiado es que ahora el bucle se cierra. Un modelo puede producir razonamiento suficiente para importar en un problema que nadie ha resuelto, los humanos pueden dirigirlo y un asistente de demostración puede certificar el resultado sin que nadie tenga que confiar en un resumen. Eso es un pipeline, no una demo, y los pipelines son lo que convierte una capacidad en una práctica.

La siguiente pregunta es si esto se generaliza más allá de los casos en los que la formalización es siquiera posible. La geometría y la dinámica tienen cierta estructura que se presta a la comprobación por máquina. Gran parte del resto de la ciencia no la tiene, y es en ese territorio más desordenado, en biología, materiales y medicina, donde la promesa de la IA como asistente de investigación se pondrá realmente a prueba. El resultado de Ghys dice que la herramienta puede funcionar. Todavía no dice con qué frecuencia.