Axiom afirma que enjambres de agentes de IA verificaron por ordenador la prueba más larga de las matemáticas — la clasificación de los grupos simples finitos — en 24 días

La startup de IA Axiom asegura haber producido la primera prueba completa verificada por ordenador de la Clasificación de los Grupos Simples Finitos (CFSG), el resultado que enumera todos los «átomos» de la simetría finita y cuya prueba humana original ocupa unas 15.000 páginas en más de 500 artículos de unos 100 matemáticos.

Cómo se hizo

Según el informe de Axiom del 26 de octubre, ingenieros y matemáticos dirigieron enjambres de decenas de agentes de IA durante 24 días (desde el 1–2 de octubre de 2026) y generaron unos 43,1 millones de líneas de código en el asistente de pruebas Lean, que comprueba cada paso lógico. El trabajo siguió la prueba de «primera generación», se apoyó en Mathlib y se dividió en 108 hitos y unas 380 tareas. Entre otras cosas, los agentes demostraron que el grupo Monstruo es simple.

Lo que encontraron las máquinas

La mayoría de los problemas hallados en la literatura eran menores (erratas, errores en tablas, hipótesis omitidas), pero Axiom informa de 34 desviaciones notables respecto a lo publicado. La mayor afecta al Teorema del Grupo No Balanceado: los agentes hallaron contraejemplos a un paso del argumento de John Walter de 1986 y el equipo construyó una ruta alternativa, con un resultado nuevo establecido por su demostrador, tras consultar a los teóricos de grupos Richard Lyons y Ronald Solomon. Axiom publicará una lista de erratas.

Advertencias

Lean verifica las deducciones, pero las personas siguen teniendo que confirmar que los enunciados y definiciones formales recogen de verdad el teorema buscado. Según informaciones de prensa al 27 de octubre, ningún grupo externo había reconstruido aún de forma independiente la prueba completa; Axiom ha publicado el repositorio y los artefactos de compilación para permitirlo. Las afirmaciones proceden del propio informe de la empresa.