Axiom Math formaliza en 24 días el «Teorema Enorme» en 43,1 millones de líneas de Lean

Axiom Math ha anunciado que ha completado la verificación por ordenador del teorema de clasificación de los grupos simples finitos (CFSG), al que los matemáticos llaman el «Teorema Enorme». Decenas de agentes de IA escribieron en 24 días unos 43,1 millones de líneas de código en Lean y formalizaron una demostración que ocupa 15 000 páginas en más de 500 artículos científicos. En ella trabajaron durante décadas unos 100 investigadores. Axiom presenta el resultado como la primera demostración completa de la CFSG que puede verificarse con un ordenador. El código y los materiales se han publicado para que cualquiera pueda examinarlos de forma independiente.

Una tabla periódica de las simetrías

La forma más sencilla de entender qué clasifica el teorema es pensar en un cubo. Se puede girar de 24 maneras distintas de modo que quede exactamente igual. Esos giros forman un grupo matemático. La CFSG describe los «bloques de construcción» fundamentales con los que se componen todos los grupos finitos de simetrías. El resultado es una especie de tabla periódica de las simetrías, que se usa en álgebra, teoría de números y física matemática.

El problema está en cómo se demostró. La demostración se fue armando a trozos, en cientos de artículos, por autores distintos y en décadas diferentes. Para una persona, revisarla entera es prácticamente imposible: habría que tener presentes miles de lemas interconectados, dispersos por distintas revistas. La formalización en Lean resuelve ese obstáculo. Cada paso del razonamiento se escribe como código, y el núcleo de Lean comprueba de forma mecánica que cada conclusión se deduce de las anteriores.

La aritmética del proyecto: 43 millones de líneas en 24 días

Las cifras dan la medida de la escala. 43,1 millones de líneas en 24 días equivalen a unos 1,8 millones de líneas al día, o unas 75 mil por hora si se cuenta el trabajo continuo, sin pausas. Cada página de la demostración en papel corresponde a unas 2 900 líneas de código formal. La formalización es varios órdenes de magnitud más detallada que el texto original, porque en los artículos los matemáticos omiten los pasos «obvios» y Lean no lo permite.

Se trata de un trabajo agéntico, no de una única generación larga. Decenas de agentes llevaron en paralelo distintas ramas de la formalización, y el código final tenía que converger en una sola demostración que el núcleo verificador aceptara. Esa comprobación por el núcleo es justo lo que distingue este resultado de la salida habitual de un modelo de lenguaje: un paso erróneo, sencillamente, no pasa.

Qué encontraron los agentes por el camino

La formalización no solo confirmó la demostración, sino que aportó hallazgos nuevos. Axiom enumera estos resultados:

• unos 43,1 millones de líneas de código en Lean, creadas en 24 días por decenas de agentes de IA;
• 34 discrepancias significativas con trabajos matemáticos publicados;
• contraejemplos a algunas afirmaciones de la literatura y demostraciones alternativas para ellas;
• un nuevo resultado en teoría de grupos, necesario para el camino de demostración elegido;
• en algunos casos, errores hallados en los razonamientos originales y nuevos argumentos matemáticos que los corrigen;
• trabajo conjunto con matemáticos, incluidos especialistas que participaron en la clasificación original.

La participación humana es aquí esencial. Cuando la formalización choca con una discrepancia respecto a la publicación, hace falta un experto que distinga una errata de un hueco real. La experiencia de los autores de la clasificación original ayudó a decidir dónde la versión formal debía seguir el original y dónde hacía falta otro camino.

Qué se puede llevar a la práctica

La principal conclusión para la industria es que los agentes que escriben y se autoverifican código en un entorno con un verificador estricto pueden abordar tareas que superan la capacidad del trabajo manual. Lean actúa como un juez que no da nada por bueno, ni de las personas ni del modelo. El mismo esquema es aplicable a cualquier ámbito donde el resultado pueda comprobarse de forma automática: la verificación de software crítico, de protocolos o de construcciones criptográficas.

Hay también una advertencia. La verificación por ordenador garantiza que la demostración es correcta con respecto a las definiciones y los enunciados que se han escrito. Por eso el código abierto importa tanto como el propio resultado: los matemáticos podrán leer las definiciones y comprobar que se ha formalizado justo lo que debía. Axiom no menciona en su anuncio el coste de esta ejecución (gasto en cómputo y tokens). Esa cifra indicará si la reverificación formal de resultados fundamentales se convertirá en rutina o se quedará en un proyecto puntual.

Para los matemáticos, la señal es clara. La literatura que antes había que aceptar por confianza en la autoridad ahora admite una reverificación mecánica completa, y por este camino ya han aparecido 34 discrepancias significativas.