Axiom, una empresa de IA dedicada a las matemáticas, anunció que su enjambre de agentes AxiomProver completó en 24 días la formalización en Lean del teorema de clasificación de los grupos simples finitos (CFSG), y asegura que es la primera demostración completa de este teorema verificada por ordenador. El código se ha publicado en GitHub con licencia Apache-2.0. El repositorio declara que la versión final no contiene marcadores sorry, no usa native_decide y depende únicamente de tres axiomas estándar: extensionalidad proposicional, el axioma de elección clásico y la solidez de los cocientes.
La clasificación de los grupos simples finitos suele llamarse “la tabla periódica de la simetría”. Establece que todo grupo simple finito pertenece a una de 18 familias infinitas o es uno de los 26 grupos esporádicos. La demostración original está repartida en más de 500 artículos, con unas 15.000 páginas, escritos por unos 100 matemáticos desde aproximadamente 1955 hasta 2004. La última pieza, la parte quasithin de Aschbacher y Smith, ocupa por sí sola 1221 páginas.
Qué ocurrió en esos 24 días
Según el relato que publicó Axiom, el proyecto creó el grupo de colaboración en Slack el 1 de octubre y los primeros agentes entraron en funcionamiento el 2 de octubre. Toda la demostración se dividió en 108 hitos y unas 380 tareas pequeñas; los agentes reclamaban tareas mediante issues de GitHub e informaban de su avance en Slack. Un agente principal se encargaba de dividir los problemas y revisar los enunciados, mientras los demás buscaban resultados existentes o escribían demostraciones en Lean, y repartían trabajo hacia abajo cuando faltaban premisas.
El proceso no fue fluido. Un primer lote de código se borró por completo debido a errores causados por suposiciones implícitas, y el equipo tuvo que replanificar. Más tarde la velocidad de compilación se convirtió en el cuello de botella: los ingenieros usaron caché y verificación en paralelo y externalizaron los cálculos finitos como certificados verificables, con lo que el build completo bajó de las 24 horas. El 10 de octubre, el proyecto anunció por separado la demostración de que el grupo Monstruo es simple.
En cuanto al corpus, Axiom dice haber leído en total 715 artículos y libros, y haber reutilizado unas 1,2 millones de líneas de código del proyecto anterior Qiuzhen-CFSG, además de bibliotecas de formalización existentes como Mathlib y Tau Ceti.
Errores detectados de paso
Durante la formalización, el equipo registró 34 desviaciones matemáticas relativamente claras. La que más atención ha recibido está en la ruta del “teorema de grupos desequilibrados” (UGT): una afirmación sobre clausuras en las memorias de Walter de 1986 tiene un contraejemplo, pues partiendo de PSL₂(49) se llega a PSL₂(7), que es justamente el grupo que esa familia excluye. También se encontró un contraejemplo, SL₂(5), para un lema de Aschbacher y Smith; al cambiar la igualdad por una desigualdad, el argumento posterior debe ampliarse.
Axiom publicó por separado un artículo de 35 páginas sobre el asunto, que propone un argumento alternativo, y reparó esta ruta con la participación de asesores como Lyons y Solomon. La empresa insiste en que estos contraejemplos no refutan el UGT en sí, y mucho menos socavan el teorema de clasificación.
“the classification remains the achievement of the mathematicians who discovered the groups”
(La clasificación sigue siendo el logro de los matemáticos que descubrieron los grupos.)
Frente a verificaciones mecánicas anteriores
En la comparación más habitual aparece la verificación del teorema del orden impar que el equipo de Gonthier completó en Coq en 2012. Ese teorema procede del artículo de 255 páginas de Feit y Thompson de 1963; el proyecto duró unos seis años y es una piedra angular de la demostración de la clasificación. Axiom cubre ahora el edificio entero, y el tiempo se mide en días.
Las velocidades no son directamente comparables. El proyecto del orden impar construyó la biblioteca prácticamente desde cero, mientras que Axiom se apoya en Mathlib y en las 1,2 millones de líneas de código CFSG anteriores; el número de agentes se describe solo como “decenas”, y la capacidad de cómputo, el hardware y el coste total que hay detrás no se han divulgado, como tampoco las horas de trabajo humano. Los 24 días son el ciclo del propio proyecto de formalización y no incluyen las décadas de trabajo humano en las que se basa.
Varias reservas también se exponen con claridad. Los metadatos del proyecto marcan la revisión como “autoevaluación”, y por ahora ningún tercero ha reproducido el build completo desde un entorno limpio. La comprobación mecánica solo garantiza que la derivación es válida a partir de las hipótesis escritas; si las definiciones del enunciado de la clasificación son fieles al teorema original sigue requiriendo que especialistas en teoría de grupos las contrasten una por una. El artículo sobre el UGT se publicó en una plataforma de preprints sin revisión por pares, y Axiom dice que la lista de erratas se publicará en la página del proyecto.
Para quienes trabajan en formalización, el siguiente paso es observar dos cosas: si la comunidad puede ejecutar de forma independiente esas 43,1 millones de líneas y cuántas de las 34 desviaciones confirman los autores originales.
Fuentes: anuncio del proyecto y repositorio de GitHub de Axiom, Unite.AI, CocoLoop, Kingy AI; el número de líneas de código Lean, declaraciones, hitos y desviaciones sigue los datos publicados por Axiom, y la duración de la verificación del teorema del orden impar procede de materiales de Microsoft Research.