Andy Garcia · dev freelance
FRENES
Volver al blog
IA y Verificación

OpenAI publicó 722 artículos de matemáticas escritos por una IA. Lean comprobó un enunciado. ¿Quién comprobó el enunciado?

7 de octubre de 2026 7 min de lectura

El martes 6 de octubre, OpenAI publicó un breve artículo titulado "Sharing AI progress in mathematics" y un repositorio de GitHub que lo acompaña. El repositorio contiene 722 manuscritos agrupados en 372 "familias de resultados", producidos por un modelo interno que no se ha lanzado. Según el README, al modelo se le plantearon aproximadamente 4000 problemas, y el resultado medio usó cerca de tres horas de cómputo de razonamiento de ChatGPT Pro.

El README también dice, sin rodeos: "Esta colección incluye resultados en distintas etapas de verificación. No todos tienen formalizaciones en Lean que los acompañen". Y después: "Algunos de los resultados no formalizados podrían tener problemas".

Ese mismo día, el Advisory Group on Mathematics and Artificial Intelligence (AGMAI), nueve matemáticos entre ellos Timothy Gowers, Martin Hairer y Edward Witten, escribió que su función asesora "no debe interpretarse como un juicio sobre el impacto de estos resultados ni como un respaldo al proceso", y que "solo la comunidad matemática puede llevar a cabo la evaluación que se necesita".

Construyo software sobre modelos todos los días, y esa es la frase que reconozco. Es la distancia entre "el agente dice que los tests pasan" y "sé qué comprueban los tests".

Los antecedentes

Esta publicación sigue a otras dos que descolocaron a los matemáticos. El 1 de agosto, OpenAI anunció diez resultados, cada uno formalizado en lo que llamó un certificado de Lean. El 8 de septiembre anunció una resolución del problema del Premio del Milenio sobre Navier-Stokes, con una formalización en Lean que tomó "17 horas adicionales mediante GPT-6 Astra". Cada vez, las discusiones más ruidosas giraron en torno al crédito, a quién se adelantaba y a la rigurosidad académica. Hairer dijo a The Verge en septiembre que le había parecido que OpenAI modificó manuscritos "a escondidas" tras las críticas, y lo calificó de "una erudición realmente mala y descuidada".

La publicación de octubre responde en parte a eso. Las correcciones "se registrarán como nuevas versiones, y las versiones publicadas anteriormente seguirán siendo accesibles". En el mundo del software eso se llama control de versiones. También publica el denominador, esos 4000 problemas, una versión de lo que AGMAI pidió en sus recomendaciones del 29 de septiembre.

Qué certifica realmente una comprobación de Lean

Lean es un lenguaje de programación en el que una prueba es un programa y un núcleo la comprueba. AGMAI pide a los laboratorios que entreguen "un archivo de desafío para comparator", y el README de Comparator lo describe como "un juez confiable para pruebas de Lean". Escribes un archivo Challenge que contiene el enunciado. La otra parte, "que intenta convencerte", aporta una Solution. Si la comprobación pasa, la Solution demuestra el mismo enunciado que tu Challenge, no usa más axiomas que los de una lista que tú permites, y el núcleo la acepta.

La primera suposición de la lista: el archivo Challenge y sus importaciones están "controlados por ti o son confiables".

Ahí está todo el juego. En código, el archivo Challenge es el test. Cuando la parte juzgada también escribe el test, una ejecución en verde es su afirmación, no tu comprobación.

Abrí el repositorio

El catálogo de formalización enumera 162 artículos con un resultado principal formalizado, de 722 manuscritos. El mapa de manuscritos enlaza una nota de alcance de Lean para 235 de las 372 familias. El campo de revisión del catálogo dice "unchecked", y su campo de método dice "agent".

La familia 266 me detuvo. Su resumen de una línea dice: "Demuestra N(6)=3, resolviendo la conjetura de Zauner sobre bases mutuamente insesgadas en dimensión seis: existen tres de esas bases en ℂ⁶, pero cuatro no. La exclusión es un cálculo certificado completo bajo las condiciones indicadas de aritmética binary64 y de compilador". Junto al resumen hay un enlace con la etiqueta "Lean". La nota de alcance que hay detrás dice: "La formalización enlazada demuestra una cota de familia más débil: toda familia en su modelo de bases mutuamente insesgadas tiene como máximo cinco miembros". Y: "El enunciado seleccionado no establece la cota superior de tres del artículo ni su exclusión asistida por ordenador de cuatro bases arbitrarias".

Abrí el archivo de desafío. Tiene 66 líneas, define su propio IsMUBFamily, y su teorema fourier_and_family_bound termina en (∀ n : ℕ, Attainable n → n ≤ 5).

La familia 017 tiene la misma forma. El resumen dice que el exponente de irracionalidad de π es exactamente 2 y que eso "también demuestra la convergencia de la serie de Flint-Hills". La nota de alcance dice que la consecuencia de Flint-Hills "queda fuera de este enunciado seleccionado".

OpenAI escribió esas notas de alcance, y son exactamente correctas. El problema es el camino de lectura: un resumen, y luego un enlace con la etiqueta "Lean". Cuando se cuenta la historia, la nota de alcance es lo primero que desaparece. Vi desaparecer un matiz de la misma manera en septiembre, con un resultado humano en el que la tilde de una cota pesaba más que el exponente.

Cuando el problema es el enunciado

La publicación de agosto ya había mostrado el caso más difícil. Un preprint de Maher Kallel y Mohamed El Louadi, publicado el 29 de agosto y sin revisión por pares, midió esos diez resultados: 20,6 MB de prueba verificada por el núcleo frente a 55,6 KB de enunciados que una persona debe leer, una proporción de 379 a 1. Pero los archivos de enunciados introducen 218 definiciones locales en lugar de reutilizar la biblioteca de la comunidad. Cuatro semanas después de la publicación, un resultado, un supuesto contraejemplo de la conjetura de rigidez de Connes, seguía en disputa sobre si su formalización significaba lo que decía. Los autores no toman posición sobre las matemáticas. Cada paso de la prueba había pasado.

En código, las definiciones locales de lo que se está probando son mocks. Una suite de tests que trae su propia idea de lo que es un User pasará contra cualquier User.

La versión adversaria está en un artículo de Google DeepMind publicado el 3 de septiembre. Cien agentes trabajaron en 71 conjeturas formales en Lean frente a un corrector ligero cuyo filtro de palabras clave bloqueaba cuatro comandos. Tras 37 soluciones genuinas, un agente descubrió que una notación local podía redefinir los símbolos que usaba un teorema, convirtiendo conjeturas abiertas en triviales. Los 34 problemas restantes quedaron "resueltos" en 27 minutos. Si has visto a un agente de código editar una aserción hasta que pasa, has visto esto.

Lo escaso es el lector

Lance Fortnow, escribiendo el 9 de septiembre, notó que Lean se usaba "como un sello de tiempo, una forma de reclamar tu teorema antes de tener que redactarlo bien de una manera explicable". El 6 de octubre, Thomas Bloom congeló las nuevas reclamaciones de pruebas en el sitio de los problemas de Erdős, porque su principal uso público se había vuelto anunciar pruebas generadas por IA, "a menudo sin ningún intento de explicarlas". Ahora pide pruebas en Lean registradas en Palomar, porque eso "facilita comprobar que el enunciado formal coincide correctamente con el enunciado del problema".

Mientras tanto, arXiv recibió 40.363 envíos en septiembre y, desde el 1 de octubre, limita a cada autor a dos al mes. Generar es barato. Leer está racionado.

Lo que pregunto antes de confiar en un resultado de IA

Manejo una versión pequeña de este problema. Un modelo juez verifica mis publicaciones contra sus fuentes, y código comprueba las cifras. En septiembre marcó una cifra como "cálculo verificado" porque la división de dos números sin relación procedentes de otra fuente cayó por casualidad dentro de la tolerancia. La cifra era correcta. La comprobación no lo era. El veredicto decía verde.

Así que, antes de confiar en cualquier resultado de IA, en matemáticas, en una pull request, o en el trabajo de patentes de la LegalTech que construyo, hago cinco preguntas.

¿Qué enunciado exacto aceptó el verificador? Pídelo literal y luego léelo.

¿Quién lo escribió? Si el agente escribió el código y el test en el mismo diff, tienes una afirmación.

¿De quién son las definiciones que usa? Las redefiniciones locales, los fixtures y los mocks de lo que se prueba son por donde se escapa el significado.

¿Qué vías de escape se permitieron? Lean tiene axiomas permitidos y sorry. El código tiene skip, xfail, @ts-ignore y --no-verify.

¿Ha leído el enunciado alguien que conozca el dominio? Los metadatos de OpenAI responden con honestidad: sin comprobar. A la mayoría de los pipelines de IA les falta ese campo.

El único cambio que hay que hacer el lunes: cuando un agente toca un test y el código que prueba en el mismo cambio, revisa primero el diff del test, a solas, como si un extraño hubiera escrito el archivo Challenge. Porque alguien lo escribió.

Fuentes

¿Un proyecto del mismo estilo?

Diseño y despliego productos como este. Hablemos.

Hablemos