✨︎ Resumen (TL;DR):
- Ocho instituciones de China formaron en Pekín una alianza de IA matemática el 11 de octubre de 2026, bajo el liderazgo de Shing-Tung Yau.
- El plan cubre modelos matemáticos, conjeturas y demostraciones formalizadas. Las fuentes describen cerca de 1,000 investigadores vinculados o una red objetivo de más de 1,000 científicos.
- La alianza establece su primer laboratorio en Qiuzhen y el Centro Yau de Tsinghua, y contempla otros en Pekín, Shanghái, Nankín, Shenzhen y Hong Kong.
Ocho instituciones de China crearon el 11 de octubre de 2026, en Pekín, una alianza encabezada por Shing-Tung Yau, ganador de la medalla Fields, para desarrollar modelos de inteligencia artificial especializados en matemáticas, incorporarlos a la investigación y facilitar la comprobación de demostraciones.
El lanzamiento ocurrió en la Universidad Tsinghua. Según la información institucional difundida por CERNET, participan, entre otras entidades, el colegio Qiuzhen, el Centro Yau de Ciencias Matemáticas de Tsinghua y el Centro Morningside de la Academia China de Ciencias.
El tamaño de la alianza aparece con dos referencias distintas. El texto atribuido a Tsinghua habla de cerca de 1,000 investigadores vinculados a las instituciones participantes. South China Morning Post describe, en cambio, una red de más de 1,000 científicos como objetivo. La primera cifra se refiere a los investigadores vinculados; la segunda, a la meta de la red.
De proponer una solución a comprobar cada paso
South China Morning Post señala como prioridades de la alianza:
- desarrollar modelos matemáticos;
- generar conjeturas;
- formalizar demostraciones;
- hacer más comprensible el razonamiento de los sistemas.
Una conjetura es una afirmación pendiente de demostración. Generarla abre una pregunta, pero todavía falta demostrarla.
La formalización matemática es un proceso que convierte una demostración en una secuencia verificable mediante definiciones, resultados previos, reglas lógicas y axiomas.
El manual oficial de Lean, un asistente de demostración, distingue entre encontrar una prueba y verificar que sea correcta. En una prueba formal, cada paso debe justificarse con definiciones, resultados previos y reglas lógicas, hasta llegar a los axiomas del sistema.
Los investigadores pueden representar esas demostraciones como objetos que otros sistemas comprueban de forma independiente. Construirlas también exige trabajo e interacción de los usuarios.
La IA explora; los matemáticos completan la prueba
El Gobierno de Pekín reprodujo una crónica de Beijing Daily sobre uno de los trabajos de geometría presentados durante el lanzamiento. El reporte describe una división de tareas: la IA ayudó a explorar estrategias de demostración y a simplificar cálculos.
A la vez, un sistema de álgebra computacional verificó identidades y produjo certificados reproducibles. Los matemáticos concibieron la prueba, revisaron los resultados y completaron la argumentación y el artículo.
El ejemplo presenta la colaboración como un proceso con tareas diferenciadas. La IA explora estrategias y realiza cálculos, mientras los investigadores revisan los resultados y completan la demostración.
Laboratorios y recursos compartidos
La alianza compartirá recursos para entrenar modelos, bibliotecas de matemáticas formalizadas y plataformas de cómputo. CERNET señala que esa infraestructura acompañará el desarrollo de modelos especializados y la investigación sobre interpretabilidad y seguridad.
- Primer laboratorio: la alianza lo establece conjuntamente en el colegio Qiuzhen y el Centro Yau de Ciencias Matemáticas de Tsinghua.
- Expansión prevista: el plan contempla otros laboratorios en Pekín, Shanghái, Nankín, Shenzhen y Hong Kong.
- Acceso: las instituciones participantes tendrán recursos abiertos para sus trabajos dentro de la alianza.
El trabajo no termina cuando la IA explora una estrategia o simplifica un cálculo. Los matemáticos todavía deben revisar la propuesta y completar la argumentación, mientras la formalización permite que otros sistemas comprueben cada paso.
