OpenAI, los problemas del milenio y el listón de la prueba

El 8 de septiembre, MIT Technology Review publicó que OpenAI ha anunciado que sus agentes han resuelto uno de los Problemas del Milenio, la lista de siete cuestiones abiertas que el Clay Mathematics Institute dotó con un millón de dólares cada una en el año 2000. En circunstancias normales, ese sería el mayor logro matemático atribuido a un sistema de IA hasta la fecha. El anuncio, sin embargo, llegó rodeado de acusaciones, y esa es la parte que conviene mirar despacio (MIT Technology Review).

Conviene situar la escala. De los siete problemas, solo uno se considera resuelto: la conjetura de Poincaré, demostrada por Grigori Perelman a principios de los 2000 y validada por la comunidad tras años de revisión. Ese es el listón, y no es un detalle burocrático. En matemáticas un resultado no existe porque alguien lo anuncie, sino cuando otras personas capaces de encontrarle el fallo no se lo encuentran. El proceso tarda meses o años, y es precisamente lo que un comunicado corporativo no puede sustituir.

El artículo detalla las acusaciones que han empañado el anuncio, y ese desenlace todavía no está escrito. Repartir razones desde fuera y con la información de un primer día sería precipitado. Lo que sí se puede analizar, y lo que se va a repetir la próxima vez, es el mecanismo: cómo se comunica un resultado de este tipo, qué se aporta como evidencia y cuánto tarda en existir una comprobación independiente.

Generar no es demostrar

La distinción importa porque los modelos actuales son extraordinariamente buenos produciendo texto con la forma de una demostración. Una prueba matemática tiene estructura, vocabulario y ritmo reconocibles, y eso es justo el tipo de patrón que un modelo aprende bien. La diferencia entre una demostración correcta y una que se rompe en el paso catorce no está en la superficie del texto: hay que seguirla línea a línea. Un revisor humano competente tarda semanas en hacerlo con un artículo largo, y los revisores capaces de auditar un problema del milenio se cuentan con los dedos.

Existe una salida técnica a ese cuello de botella y no es nueva: la formalización. Asistentes de prueba como Lean, con su biblioteca mathlib, permiten escribir matemáticas en un lenguaje que una máquina verifica de forma exhaustiva. Si una demostración compila en Lean, es correcta, sin comité y sin buena fe de por medio. En 2024 DeepMind mostró con AlphaProof que un sistema podía razonar dentro de ese marco a nivel de medalla de plata en la Olimpiada Internacional de Matemáticas.

Por eso la pregunta relevante ante cualquier anuncio de este tipo no es si el modelo es potente, sino en qué formato se ha entregado el resultado y quién lo ha comprobado. Si hay artefacto formal verificable, la discusión se cierra rápido y en público. Si lo que hay es un PDF y una nota de prensa, el calendario lo marca la revisión por pares, no el departamento de comunicación.

Qué se lleva de aquí quien trabaja con agentes

La lección salta del terreno matemático al de cualquiera que ponga agentes a producir. Un agente genera salidas plausibles con una fluidez que desarma, y la plausibilidad no es corrección. En desarrollo eso se gestiona con tests, tipos y CI: el modelo propone y una máquina dictamina. En dominios sin verificador automático, el coste de comprobar crece hasta comerse la ganancia de velocidad, y ahí es donde muchos despliegues se atascan sin admitirlo del todo.

De ahí que el trabajo aburrido, montar el verificador antes que el generador, siga siendo el que más rinde. Definir qué cuenta como resultado válido, automatizar esa comprobación y dejar que el agente itere contra ella es lo que separa un piloto que impresiona en una demo de algo que se puede dejar corriendo en producción.

Nuestra postura es sosa a propósito: los anuncios se leen, los resultados se verifican, y entre una cosa y otra caben meses. El artículo de MIT Technology Review hace bien en no zanjar el asunto, porque quien tiene que zanjarlo es la comunidad matemática y no una sala de prensa.