Los agentes de IA de Axiom formalizan la clasificación de los grupos finitos simples en Lean

Axiom Math dijo el 26 de octubre de 2026 que ha publicado la primera prueba completa verificada por computadora de la Clasificación de los Grupos Finitos Simples, escrita en el asistente de pruebas Lean [1]. Durante 24 días, sus ingenieros y matemáticos dirigieron enjambres de docenas de agentes de IA que produjeron alrededor de 43,1 millones de líneas de código Lean [1][2].

¿Qué formalizó Axiom?

La clasificación, a menudo llamada el teorema enorme, enumera los bloques de construcción de todos los grupos finitos, las matemáticas de la simetría [1]. Afirma que todo grupo finito simple es cíclico de orden primo, alternante, de tipo Lie o uno de 26 grupos esporádicos [2].

Axiom dice que la prueba original abarca aproximadamente 15.000 páginas en más de 500 artículos de unos 100 matemáticos [1]. Su versión en Lean sigue la prueba de primera generación y, según la página de GitHub del proyecto, está libre de disculpas, lo que significa que ningún paso queda sin probar [3].

Axiom dice que sus agentes de IA produjeron alrededor de 43,1 millones de líneas de Lean en 24 días para formalizar la clasificación. El sitio del proyecto lista 2,05 millones de declaraciones y 715 artículos y libros en el corpus [2]. Axiom dice que la formalización incorpora alrededor de 1,2 millones de líneas de un proyecto anterior, Qiuzhen-CFSG, y se basa en la biblioteca Mathlib [1].

¿Cómo funcionó el enjambre de agentes?

Axiom abrió un canal de Slack para el proyecto el 1 de octubre de 2026 y el primer enjambre entró en funcionamiento el 2 de octubre [1]. Un mapa de prueba extraído de la literatura dividió el trabajo en 108 hitos y unas 380 tareas más pequeñas, que los agentes reclamaron a través de incidencias de GitHub [1].

Los agentes principales desglosaron argumentos difíciles y revisaron declaraciones, mientras que otros buscaron resultados existentes o escribieron pruebas en Lean [1]. Los matemáticos humanos manejaron obstrucciones matemáticas y los ingenieros mantuvieron el sistema en funcionamiento [1]. Axiom dice que eliminó decenas de miles de líneas basadas en suposiciones no probadas y reinició partes del trabajo [1].

El 10 de octubre, según Axiom, un mensaje en el canal anunció que los agentes habían probado que el grupo Monstruo es simple [1]. Lean verifica las deducciones, mientras que los humanos inspeccionan la declaración final y las definiciones para confirmar que expresan el teorema previsto [1].

¿Qué errores encontraron los agentes de IA?

Axiom dice que la mayoría de los problemas que encontró fueron menores, como errores tipográficos, errores en tablas o hipótesis omitidas [1]. Axiom encontró 34 desviaciones notables respecto al registro publicado que necesitaban resolverse. El caso más sustancial concernía al Teorema del Grupo Desequilibrado [1][2].

Allí, los agentes encontraron contraejemplos a una afirmación de cierre en el argumento de John Walter de 1986, lo que dejó un paso clave sin justificar sin refutar el teorema en sí [1]. Un argumento alternativo basado en la teoría de 1976 de Ronald Solomon sobre los 2-componentes maximales se convirtió en un nuevo resultado, escrito en un artículo de 35 páginas [1][2]. Solomon y Richard Lyons, que trabajaron en la clasificación original, fueron consultados [1].

¿Alguien fuera de Axiom ha verificado la prueba?

Todavía no, según RuntimeWire [4]. Carina Hong, CEO de Axiom, dijo a RuntimeWire que ningún grupo externo ha reconstruido y verificado aún la prueba. Axiom está publicando los artefactos de compilación para que otros puedan reproducirla [4].

La página de GitHub dice que un solo comando de compilación verifica todo el proyecto, y que Axiom usó cambios pendientes en Lake, la herramienta de compilación de Lean, para mantener el tiempo de compilación por debajo de 24 horas [3]. The AI Pin cubrió las afirmaciones separadas de OpenAI sobre nuevos descubrimientos matemáticos el 27 de octubre.

Nuestra lectura

Opinión: Auditar una prueba que ninguna persona ha leído completamente es un uso más convincente de la IA en matemáticas que perseguir titulares nuevos, y encontrar 34 desviaciones reales muestra que la auditoría tuvo dientes. Sin embargo, el resultado solo es tan fuerte como sus verificaciones externas, por lo que una reconstrucción independiente y una revisión de erratas en teoría de grupos importan más que el recuento de líneas.

Lo que no pudimos verificar

• Si la prueba de 43,1 millones de líneas se compila y verifica fuera de Axiom; según RuntimeWire, ningún grupo externo había completado una reconstrucción hasta el 27 de octubre de 2026.
• Qué modelos de IA impulsaron a los agentes; Axiom solo dice que usaron una mezcla cambiante de modelos.
• Cómo juzgan el resultado los teóricos de grupos independientes; no encontramos ninguna reacción publicada de un teórico de grupos fuera del círculo asesor de Axiom en el momento de la publicación.
• La lista completa de las 34 desviaciones notables; Axiom dice que publicará la lista de erratas después de consultar a los teóricos de grupos.
• Si el nuevo artículo sobre el Teorema del Grupo Desequilibrado se sostiene bajo revisión por pares; está publicado en Hexagon, y no pudimos confirmar ninguna revisión por pares de revista.