Axiom Math asegura que agentes de IA han formalizado en Lean la clasificación de los grupos simples finitos

Axiom Math, una start-up estadounidense que desarrolla sistemas de IA para matemáticas, anunció el 26 de octubre de 2026 que había obtenido una prueba completa verificada por máquina de la clasificación de los grupos simples finitos, uno de los resultados más largos de las matemáticas. El trabajo se hizo en Lean, un asistente de demostración cuyo núcleo comprueba cada paso lógico.

Qué dice haber logrado Axiom

La clasificación establece que todo grupo simple finito es cíclico de orden primo, alternado, de tipo Lie o uno de los 26 grupos esporádicos. Su prueba original, completada por muchos autores durante décadas, ocupa miles de páginas de revistas. Axiom formalizó esta prueba de primera generación; una prueba de segunda generación, que se publica en una serie de volúmenes, sigue sin terminar.

Según la entrada de blog de la empresa, decenas de agentes que funcionan sobre su sistema AxiomProver hicieron la mayor parte de la escritura en 24 días. Unos agentes principales descomponían los argumentos y revisaban los enunciados, mientras otros buscaban resultados existentes o redactaban pruebas en Lean, con una combinación cambiante de modelos. Ingenieros y matemáticos dirigieron el trabajo, estudiaron los obstáculos matemáticos y se ocuparon de los problemas de mayor alcance. Unite.AI informa de que el primer enjambre arrancó el 2 de octubre. La página del proyecto recoge unos 43,1 millones de líneas de Lean y 2,05 millones de declaraciones, y el código está publicado en GitHub.

Errores en la literatura publicada

Axiom identifica 34 desviaciones relevantes respecto a la literatura, en su mayoría menores, como erratas, fallos en tablas u omisión de hipótesis. La más importante afecta a la demostración del teorema de los grupos no equilibrados (Unbalanced Group Theorem) de John Walter, donde los agentes hallaron contraejemplos a una afirmación en la que se apoyaba el argumento. Axiom dice que subsanó el hueco con ayuda de un nuevo resultado y que consultó a los especialistas Richard Lyons y Ronald Solomon. También señala una igualdad falsa en un lema de los volúmenes de Aschbacher y Smith sobre grupos «quasithin». Según la empresa, nada de esto invalida el teorema, y ha publicado la lista completa de erratas.

Cautelas

Todas las cifras proceden de materiales de Axiom, y la página de estadísticas del proyecto no es del todo coherente: por ejemplo, ofrece recuentos distintos de hitos y de obras fuente en diferentes lugares. Por ahora no se cita ninguna evaluación independiente. Como recuerda la empresa, Lean verifica las deducciones, pero son las personas quienes deben comprobar que el enunciado formal y las definiciones reflejan fielmente las matemáticas. Axiom, cofundada por Carina Hong y Shubho Sengupta, captó 64 millones de dólares en 2025.