Axiom Math publica una demostración en Lean de 43,1 millones de líneas sobre la clasificación de grupos

Axiom Math anunció el 27 de octubre de 2026 que publicará lo que denomina la primera demostración completa de la Clasificación de los Grupos Finitos Simples verificada por computadora. Un equipo de ingenieros y matemáticos la produjo en 24 días, dirigiendo enjambres de decenas de agentes de IA que escribieron aproximadamente 43,1 millones de líneas de código en el asistente de demostración Lean.

«Hoy publicamos la primera demostración completa de la Clasificación de los Grupos Finitos Simples (CFSG) verificada por computadora», escribió la empresa en su anuncio. La clasificación identifica los bloques básicos que componen los grupos finitos. Su demostración original abarca unas 15.000 páginas distribuidas en más de 500 artículos de alrededor de 100 matemáticos, una escala que le valió el apodo de «teorema enorme».

Qué publicó Axiom

La CFSG establece que todo grupo finito simple es cíclico de orden primo, alternante sobre al menos cinco símbolos, pertenece a una de dieciséis familias infinitas de grupos de tipo Lie construidos sobre cuerpos finitos o es uno de exactamente 26 grupos esporádicos aislados; el anuncio señala que algunos autores cuentan el grupo de Tits como un vigesimoséptimo. El mayor grupo esporádico, el Monstruo, fue construido por Robert Griess en 1980 mediante un álgebra de dimensión 196.884.

El esfuerzo humano para demostrar el teorema se prolongó durante décadas. En 1963, Walter Feit y John Thompson demostraron que todo grupo finito simple no abeliano tiene orden par, en un artículo de 255 páginas que ocupó un número entero de Pacific Journal of Mathematics. En 1972, Daniel Gorenstein presentó un programa de dieciséis pasos para completar la clasificación y en 1983 declaró que estaba terminada. Sin embargo, el caso cuasidelgado se basaba en un manuscrito inacabado de Geoffrey Mason, hasta que Michael Aschbacher y Stephen Smith publicaron en 2004 un estudio de 1.221 páginas que cerró lo que llegó a conocerse como la demostración de primera generación. Una demostración de segunda generación, más sistemática, iniciada por Gorenstein y Richard Lyons, a quienes después se unieron Ronald Solomon e Inna Capdeboscq, sigue incompleta; por eso, Axiom formalizó la demostración de primera generación.

La página del proyecto presenta la formalización como una versión de la demostración de primera generación en la que el núcleo de Lean comprueba cada paso lógico. También indica que el corpus contiene 43,1 millones de líneas de Lean, 2,05 millones de declaraciones y 715 artículos y libros. Axiom afirma que el mapa de la demostración se basó en los volúmenes de segunda generación y que la formalización incorpora aproximadamente 1,2 millones de líneas de código del proyecto anterior Qiuzhen-CFSG y se apoya en Mathlib, cuya creación atribuye a cientos de colaboradores. El proyecto menciona a Dean Cureton, Vasily Ilin, Bhavik Mehta y Niels Voss como colaboradores principales, y a Letong Hong como investigador principal.

El repositorio público de GitHub describe el resultado como una demostración en Lean4 sin uso de sorry, fijada en la versión 4.35.0-rc3, construida sobre Mathlib y el proyecto TauCeti y que utiliza únicamente los axiomas estándar Classical.choice, propext y Quot.sound, sin native_decide. Su enunciado formal de la clasificación, tomado de TauCeti, dice: «Todo grupo finito simple es isomorfo a uno de los grupos construidos explícitamente que aparecen en la lista de clasificación». El archivo README indica que lake build comprueba todo el desarrollo y que los cambios en curso en la herramienta de compilación Lake, junto con las optimizaciones que el equipo planea incorporar al proyecto, redujeron el tiempo de compilación a menos de 24 horas. El código cuenta con una licencia Apache-2.0.

Un esfuerzo colectivo de 24 días

El 1 de octubre de 2026, Axiom abrió un canal de Slack para coordinar el proyecto. El trabajo previo en Lean y un mapa interno de la demostración, elaborado a partir de la bibliografía publicada, dividieron el esfuerzo en 108 hitos y unos 380 encargos más pequeños. El primer enjambre se puso en marcha el 2 de octubre de 2026: los agentes se asignaban hitos mediante incidencias de GitHub e informaban de las tareas completadas en Slack. Los agentes principales desglosaban los argumentos difíciles y revisaban los enunciados, mientras que otros buscaban resultados existentes o escribían demostraciones en Lean. Además, un agente podía delegar en otros la búsqueda de requisitos previos que faltaban, y sus resultados se incorporaban a un repositorio compartido.

Los primeros avances dejaron al descubierto puntos débiles. Algunos hitos que parecían manejables escondían requisitos previos enormes que los agentes habían dado por supuestos en lugar de demostrar. El equipo tuvo que borrar decenas de miles de líneas basadas en esas suposiciones antes de retomar el trabajo con un plan más sólido. Uno de los primeros hitos se refería al teorema del funtor de señalizador, cuya demostración propuesta dependía de supuestos estructurales que aún debían justificarse. Los tiempos de compilación también se convirtieron en un cuello de botella: los agentes producían demostraciones más rápido de lo que Lean podía volver a comprobarlas. Axiom afirma que sus ingenieros distribuyeron entre varios trabajadores los resultados de compilación almacenados en caché, ejecutaron comprobaciones independientes en paralelo y externalizaron los cálculos finitos costosos mediante certificados verificables por separado. Según la empresa, estos cambios aceleraron la verificación en varios órdenes de magnitud.

El 10 de octubre de 2026, un mensaje en el canal anunció que los agentes habían demostrado que el Monstruo es simple, relata la empresa. Los agentes también formalizaron la existencia del Monstruo mediante el álgebra de Griess y un teorema que identifica con el Monstruo a los grupos de tipo Monstruo. El 13 de octubre de 2026 solo se completó un hito, por lo que los ingenieros organizaron una nueva planificación y dividieron los hitos pendientes en teoremas más pequeños y formulados con precisión. Cada descomposición debía mostrar, mediante una breve demostración en Lean, cómo las partes permitirían establecer el hito original.

Lagunas detectadas en la demostración publicada

La traducción de la demostración a Lean dejó al descubierto problemas en los argumentos publicados, informa Axiom. La mayoría eran menores —errores tipográficos, errores en tablas u omisiones de hipótesis—, pero la empresa contabiliza 34 discrepancias destacables respecto del texto publicado; la más importante se refiere al teorema de grupos no equilibrados, o UGT.

Un ejemplo se encontró en los volúmenes de Aschbacher y Smith sobre grupos cuasidelgados, donde un lema afirmaba que dos cantidades numéricas eran iguales. Los agentes hallaron un contraejemplo relacionado con el grupo SL₂(5), en el que una cantidad era 1, cuando la igualdad afirmada exigía que fuera 2. Sustituir la igualdad por una desigualdad corrigió el lema, pero argumentos posteriores se habían basado en la igualdad para descartar casos, por lo que el equipo amplió un argumento anterior para abarcar esas configuraciones.

El UGT permite identificar un grupo completo a partir de información sobre sus subgrupos: según el resumen de el artículo adjunto, bajo las hipótesis inductivas de la clasificación, si un subgrupo no trivial de orden impar es normal en el centralizador de una involución, el grupo simple que lo contiene debe ser de tipo Lie en característica impar o alternante de ciertos grados. Axiom abordó el UGT a partir de las memorias de John Walter de 1986 y, al formalizar ese argumento, sus agentes encontraron contraejemplos explícitos a una afirmación de clausura que este utilizaba: una operación que, según se suponía, mantenía los grupos simples asociados dentro de una familia determinada podía producir un grupo expresamente excluido de ella.

Según la explicación de la empresa, al partir de PSL₂(49), cuya involución de cuerpo tiene como centralizador PGL₂(7), la operación produce el componente simple PSL₂(7), que queda excluido de la familia porque 7 es un primo de Mersenne. Axiom señala que los contraejemplos no refutaban el UGT en sí ni siquiera la conclusión de la Proposición II.5.9(ii) de Walter.

La corrección se basó en la teoría de Solomon de 1976 sobre los 2-componentes maximales, que, según Axiom, aportó las ideas centrales para un argumento alternativo generado y formalizado por su sistema AxiomProver. El paso clave, presentado en el artículo como el Teorema 2.3 (preservación de las cimas simples), es descrito por Axiom como un nuevo resultado de teoría de grupos demostrado por AxiomProver; junto con las reducciones de Gilman y Solomon y los teoremas de reconocimiento de Foote y Harris, proporciona la formulación del UGT para grupos simples que necesita la clasificación. Tras la formalización, los matemáticos de Axiom encontraron una deducción más breve, basada en métodos de primera generación y recogida como Observación 9.5, que llega a la misma conclusión sin el Teorema 2.3.

Ese artículo, The Unbalanced Group Theorem, escrito por Colin Defant y Ken Ono, apareció en el servidor de prepublicaciones Hexagon como versión 1 el 27 de octubre de 2026, bajo una licencia CC BY 4.0; la página del proyecto indica que tiene 35 páginas. Axiom afirma que está colaborando con especialistas en teoría de grupos para recopilar las erratas detectadas en la bibliografía y que las publicará en la página de erratas del proyecto. Se consultó a Lyons y Solomon, cuyo trabajo sustenta la clasificación, sobre la corrección del UGT, y la empresa afirma que seguirá recopilando y resolviendo las erratas con la ayuda de un consejo asesor que los incluye, junto con el asesor externo Dan Nakano. Axiom presenta su contribución como una forma de hacer que la demostración pueda verificarse mecánicamente, documentar los obstáculos encontrados y aportar argumentos formalizados para resolverlos, y señala que la clasificación sigue siendo un logro de los matemáticos que descubrieron los grupos y desarrollaron los argumentos.