OpenAI publica en GitHub 722 trabajos de matemáticas generados por un modelo no publicado

Hace unos días, OpenAI publicó en GitHub 722 trabajos de matemáticas generados por un modelo frontier interno que todavía no se ha lanzado. Los temas son teoría de números, geometría algebraica, análisis y combinatoria. Parte de los resultados va acompañada de demostraciones formales en Lean. El medio chino Jiqizhixin describe las consecuencias sin rodeos: la IA ha empezado a producir matemáticas nuevas más rápido de lo que los matemáticos pueden entenderlas, y la comunidad necesitará años para digerirlo todo.

Qué se ha publicado exactamente

La escala llama la atención por sí sola. Más de setecientos trabajos en un solo paquete, y en varias ramas de las matemáticas a la vez. Normalmente, un volumen así se acumula durante años y con decenas de autores.

El fragmento disponible del material se interrumpe en la descripción del repositorio. Por eso se desconocen varios detalles importantes: cómo están organizados los archivos, bajo qué licencia se han publicado los textos, cuántas personas participaron en la selección y si los trabajos pasaron por revisión por pares. OpenAI no ha lanzado el modelo, así que no es posible reproducir el resultado desde fuera.

• 722 trabajos en un repositorio abierto en GitHub
• Fuente: un modelo interno no publicado de OpenAI
• Áreas: teoría de números, geometría algebraica, análisis, combinatoria
• Parte de los trabajos cuenta con verificación formal en Lean
• Estado de la revisión experta independiente: no se indica en el material disponible

El cuello de botella se ha desplazado a la verificación

Aquí Lean funciona como una red de seguridad. Es un sistema de demostraciones en el que un compilador comprueba cada paso. Si la demostración compila, no contiene lagunas lógicas. Pero quedan preguntas que la máquina no resuelve. ¿Se ha formalizado exactamente el enunciado que se afirma en el artículo? ¿Es interesante el resultado o se trata de un corolario menor de algo ya conocido? ¿Encaja en una línea de investigación activa?

Para los trabajos sin formalizar, el panorama es peor. Los lee una persona, y la revisión de un solo artículo complejo lleva semanas, a veces meses. 722 textos convierten esa cola en un problema que no se resuelve contratando a un par de revisores más.

La segunda parte del titular de Jiqizhixin afirma que los matemáticos se han quedado sin proyectos de investigación. El mecanismo es sencillo. Si el modelo cierra un problema en el que un doctorando pensaba trabajar durante año y medio, el tema pierde valor antes de que pueda defender su tesis. Es una valoración del medio, no un hecho confirmado sobre personas concretas, pero la lógica se entiende. Corren más riesgo quienes trabajan en problemas técnicos y fácilmente formalizables.

Cómo trabajar con esto

Los matemáticos deberían contrastar sus líneas de trabajo actuales con el repositorio. Conviene encontrar ahora las coincidencias, y no después de enviar un preprint. Además, tiene sentido aprender Lean al menos a nivel de lectura: la capacidad de verificar rápido una formalización ajena se está convirtiendo en una habilidad profesional.

Las revistas y las plataformas del tipo arXiv tendrán que definir una política. Deberán decidir si aceptan textos escritos por un modelo y si exigen una demostración formal como condición para evaluarlos. Sin ello, el flujo de trabajos generados por máquinas simplemente saturará la cola.

Para ingenieros y responsables de equipos hay una conclusión más amplia. La verificación formal sale del nicho académico y se convierte en una forma de aceptar resultados de la IA sin fiarse de su palabra. El mismo principio se aplica al código y a los sistemas críticos.

Por último, mientras no haya análisis independientes, conviene abstenerse de sacar conclusiones grandilocuentes. El indicador clave para los próximos meses es qué proporción de los 722 trabajos supera la verificación y cuántos resultan sustanciales, y no meramente correctos.