OpenAI publica 719 manuscritos matemáticos, con Lean en el 42 % de los resultados principales

OpenAI ha abierto un repositorio con 719 manuscritos matemáticos agrupados en 372 familias. El README explica que la gran mayoría se produjo con el mismo procedimiento: un modelo interno no publicado recibió unos 4.000 problemas abiertos y empleó una media de tres horas de computación de ChatGPT Pro thinking por cada resultado encontrado.

Un solo modelo convirtió problemas abiertos en una serie editorial

El repositorio incluye PDF, archivos fuente, datos de citación y artefactos de apoyo para las pruebas. OpenAI señala que algunos resultados amplían trabajos anteriores de sus modelos y que los materiales están en distintas fases de verificación. También publicó resúmenes abreviados del razonamiento para diez familias seleccionadas.

La entrega inicial contenía 722 manuscritos. El catálogo actual registra 719 tras la retirada de tres. Zvi Mowshowitz destaca la amplitud y afirma que el conjunto incluye 90 problemas entre los 500 primeros de Proof of Atlas. Es una valoración externa de su importancia, no una clasificación de OpenAI.

El recurso escaso ya no es el primer borrador de la prueba

Si un modelo puede producir cientos de resultados candidatos, el trabajo matemático se desplaza hacia la verificación, la explicación y la incorporación al campo. Un manuscrito puede contener una idea correcta, pero el valor científico llega cuando los expertos entienden los supuestos, comparan el resultado con la literatura y pueden construir sobre él.

Eso cambia la economía de la investigación. La generación escala con computación, mientras que la lectura cuidadosa sigue consumiendo el tiempo de especialistas escasos. Una publicación masiva crea conocimiento y también una cola de trabajo para una comunidad que no controla el modelo ni puede interrogar a su autor.

Lean comprueba un enunciado formal, no toda la historia científica

OpenAI informa de formalizaciones en Lean para cerca del 42 % de los resultados principales y admite que los trabajos no formalizados pueden contener problemas. Los tres manuscritos retirados poco después de la publicación muestran por qué importa distinguir una prueba candidata de un resultado aceptado.

Incluso una formalización válida no resuelve todas las preguntas. Hay que comprobar que el enunciado formal coincide con el problema abierto conocido, que no faltan condiciones importantes y que el resultado encaja en la matemática existente. Por eso AGMAI describió la publicación como el inicio de la comprensión humana, no como su final.

El ritmo de correcciones dirá si el repositorio funciona como ciencia

La historia de revisiones, la proporción de nuevas formalizaciones, las reproducciones independientes y una exposición clara dirán más que el número de PDF. OpenAI promete conservar las versiones públicas y seguir añadiendo pruebas en Lean, lo que permitirá ver qué afirmaciones resisten y con qué rapidez se corrigen los errores.

La participación de la comunidad será la segunda prueba. Si los matemáticos obtienen herramientas, computación y espacio para formular sus propias preguntas, el repositorio puede acelerar el campo. Si heredan sobre todo la revisión de cientos de textos difíciles, el modelo habrá acelerado la producción de manuscritos y enviado a otros la factura de entenderlos.

El veredicto de Lilith

OpenAI ha dejado 719 cajas de manuscritos en la biblioteca. Ahora veremos si contienen nuevos mapas de las matemáticas o, sobre todo, turnos extra para quienes revisan pruebas.