Agentes de IA formalizaron en 24 días 15 000 páginas de demostraciones y encontraron un fallo

Varias decenas de agentes de IA convirtieron en 24 días una demostración de unas 15 000 páginas en más de 43 millones de líneas de código, que el ordenador comprueba paso a paso. Matemáticos de primer nivel llevaban décadas trabajando en ese texto, una de las construcciones más grandes de la historia de las matemáticas. De paso, el sistema encontró en el razonamiento de los autores un vacío lógico que existía desde hacía casi 40 años.

Una página de tres mil líneas

Formalizar una demostración significa escribir de forma explícita cada paso que el matemático omite en el artículo con un «como es fácil comprobar». Después, un programa verificador tiene que aceptar ese registro. Si en la cadena hay un hueco, el código simplemente no pasa la comprobación.

La aritmética da la medida de la escala. 43 millones de líneas entre 15 000 páginas salen a unas 2 900 líneas por página. En 24 días, eso supone del orden de 1,8 millones de líneas al día, o unas 75 000 por hora sin parar. Un equipo humano no habría podido con estos volúmenes: formalizar incluso teoremas pequeños suele llevar meses a los especialistas.

Por qué fue una máquina la que encontró el hueco

El vacío de casi 40 años sobrevivió a decenas de lectores atentos. No se debe a descuido por su parte. Revisar 15 000 páginas a mano es inviable: el revisor se apoya en la autoridad de los autores y en que los pasos intermedios son lo bastante obvios. El verificador no concede ese crédito de confianza. Cada transición, o la acepta, o la rechaza.

Por eso la formalización funciona también como auditoría. El agente que intenta codificar un paso se topa con el punto donde falta la justificación. Para las matemáticas es una señal seria: afecta a la integridad de todo el edificio, no a un retoque cosmético.

Economía: cuántos tokens cuesta una obra así

Esta es una estimación de la redacción, no un dato del proyecto. Con 10–12 tokens por línea, el código final supone unos 500 millones de tokens de salida. El gasto real es mucho mayor, porque los agentes escriben borradores, reciben los errores del verificador, reescriben y vuelven a comprobar. Con esas iteraciones, la cuenta probablemente se mide en miles de millones de tokens.

Aun así, el plazo de 24 días se logró gracias al paralelismo. Una demostración grande se descompone de forma natural en un grafo de lemas con dependencias, y las ramas independientes pueden repartirse entre distintos agentes a la vez. El verificador actúa aquí como árbitro con respuesta binaria, «aceptado o no», de modo que los agentes no tienen que fiarse unos de otros por su palabra.

Cifras clave del proyecto:

• unas 15 000 páginas de demostración original, reunidas a lo largo de décadas;
• 24 días de trabajo del sistema;
• varias decenas de agentes trabajando en paralelo;
• más de 43 millones de líneas de código verificable;
• unos 1,8 millones de líneas al día de media;
• unas 2 900 líneas de código por página de texto;
• un vacío en la argumentación de casi 40 años de antigüedad.

Qué se puede llevar a la práctica de ingeniería

La lección principal no atañe solo a las matemáticas. Los sistemas de agentes escalan mejor allí donde existe un comprobador automático inequívoco: un compilador, un conjunto de tests, un motor de demostración. En ese caso, cientos de miles de líneas generadas no requieren revisión manual, porque la criba la hace la máquina.

El mismo esquema vale para la verificación formal de bibliotecas criptográficas, compiladores, protocolos de consenso y bloques de hardware. Las condiciones son siempre las mismas: una especificación detallada, un verificador estricto y la posibilidad de dividir el trabajo en piezas independientes. Para los equipos que planean pipelines de agentes, de aquí se desprende una conclusión práctica. Conviene empezar invirtiendo en el verificador y en la descomposición de la tarea; el número de agentes y el tamaño del modelo son secundarios. Hay otra conclusión para la revisión por pares: una demostración formalizada ofrece una garantía reproducible que un texto manuscrito de 15 000 páginas no puede dar.