Agentes de IA tradujeron una demostración de 15.000 páginas a 43 millones de líneas de código en 24 días — y encontraron un error de hace 40 años

Traducir una montaña de matemáticas a algo que una máquina pueda verificar

Un equipo de varias decenas de agentes de IA tardó 24 días en reescribir una de las demostraciones matemáticas más voluminosas de la historia —unas 15.000 páginas de texto en las que los principales matemáticos habían trabajado durante décadas— en un formato comprensible para una computadora: más de 43 millones de líneas de código, verificadas paso a paso por un programa verificador. En el proceso, los agentes descubrieron un vacío lógico en el razonamiento que había pasado desapercibido durante casi 40 años.

Qué significa "formalizar" una demostración

Un artículo matemático convencional está escrito para humanos y está lleno de frases como "es fácil comprobar que" o "es evidente que" —el autor omite pasos intermedios, confiando en que un lector experto los reconstruirá por su cuenta. La formalización exige escribir explícitamente cada uno de esos pasos, sin lagunas, en forma de código que luego verifica un programa especializado. Si en la cadena de razonamiento hay un agujero, el código simplemente no pasa la verificación: aquí no hay término medio.

La escala de la operación se aprecia en una aritmética sencilla: 43 millones de líneas de código para un documento fuente de 15.000 páginas equivalen a unas 2.900 líneas por cada página de texto. En 24 días de trabajo, eso se traduce en aproximadamente 1,8 millones de líneas al día, es decir, unas 75.000 líneas por hora de trabajo ininterrumpido. Como comparación, formalizar manualmente incluso teoremas de tamaño modesto suele llevarle meses a especialistas humanos: un equipo de matemáticos jamás podría asumir ese volumen a mano.

Por qué fue una máquina, y no los humanos, quien encontró el agujero

en la demostración

El vacío en el razonamiento que detectaron los agentes sobrevivió a decenas de revisores atentos durante casi 40 años. Esto no delata negligencia por parte de esas personas, sino que revela la naturaleza misma de la revisión manual. Leer 15.000 páginas de principio a fin y volver a comprobar cada transición lógica es físicamente irrealizable. Un revisor inevitablemente se apoya en la reputación de los autores y en la sensación intuitiva de que un paso intermedio "parece correcto".

El verificador simplemente no tiene esa confianza a su disposición. Cualquier transición de una afirmación a otra la acepta como rigurosamente demostrada o la rechaza. Cuando un agente de IA intenta codificar el siguiente paso de la demostración, antes o después se topa con un punto donde falta justificación, y a partir de ahí el código sencillamente no compila. Para la comunidad matemática esto es una señal seria, no una objeción formal: está en juego la integridad de toda una construcción que se consideraba terminada desde hacía décadas.

Cuánto cuesta esto en tokens

Esta es una estimación de la redacción de Hamidun News, no datos oficiales del proyecto. Calculando entre 10 y 12 tokens por cada línea de código final, los 43 millones de líneas resultantes equivalen a unos quinientos millones de tokens solo en la salida terminada. El gasto real es considerablemente mayor: los agentes escriben versiones preliminares, reciben errores del verificador, reescriben fragmentos y vuelven a ejecutar la verificación. Teniendo en cuenta todas esas iteraciones, la cifra probablemente se cuenta ya en miles de millones de tokens.

El plazo reducido de 24 días fue posible gracias al trabajo en paralelo. Una demostración grande se descompone de forma natural en un grafo de lemas con dependencias entre sí, y las ramas independientes de ese grafo pueden repartirse entre distintos agentes simultáneamente. El verificador, mientras tanto, funciona como árbitro imparcial con una respuesta binaria de "aceptado" o "rechazado": por eso los agentes no necesitan fiarse de los resultados de los demás por su palabra, ya que cualquier fragmento de código pasa la verificación o no la pasa.

Qué pueden aprovechar de esto los equipos de ingeniería

La lección principal no se limita a las matemáticas puras. Los sistemas agénticos escalan mejor allí donde existe un juez automático inequívoco: un compilador, una batería de pruebas o un motor de demostración. En esas condiciones, cientos de miles de líneas de código generadas no necesitan revisarse a mano, porque la propia máquina se encarga del filtrado.

El mismo esquema es aplicable a la verificación formal de bibliotecas criptográficas, compiladores, protocolos de consenso y bloques de hardware. Las condiciones son las mismas en todos los casos: una especificación detallada de la tarea, un verificador automático estricto y la posibilidad de dividir el trabajo en bloques independientes. Los equipos que planeen construir pipelines agénticos similares deberían invertir sobre todo en el propio verificador y en la descomposición de la tarea en bloques independientes; el número de agentes y el tamaño del modelo son aquí secundarios.

Y una última conclusión práctica tiene que ver con la revisión por pares: una demostración formalizada ofrece una garantía reproducible de corrección que un texto manuscrito de 15.000 páginas simplemente no puede dar.