Axiom anuncia haber verificado en Lean la clasificación de los grupos finitos simples, la prueba más larga de las matemáticas

La start-up Axiom afirma haber hecho verificable por ordenador la clasificación de los grupos finitos simples (a menudo abreviada CFSG), apodada « el teorema enorme »: una prueba de unas 15 000 páginas, repartida en más de 500 artículos escritos por un centenar de matemáticos a lo largo de varias décadas. El anuncio cayó en X este martes 27 de octubre a las 15:34, hora de París, acompañado de una larga entrada de blog fechada el día anterior, de un mapa de prueba interactivo y de un repositorio de código.

De qué se trata

Un grupo describe simetrías, como las 24 rotaciones que dejan un cubo inalterado. Los grupos finitos se descomponen en « ladrillos » indivisibles, los grupos simples, un poco como los números enteros en números primos. La clasificación dice que la lista de estos ladrillos es completa: grupos cíclicos de orden primo, grupos alternados (sobre al menos cinco elementos), dieciséis familias infinitas de grupos « de tipo de Lie » y exactamente 26 grupos esporádicos, de los cuales el más grande, el grupo Monstruo. Este resultado sirve en numerosos campos (álgebra, teoría de números, combinatoria), pero muy pocas personas pueden verificar el conjunto.

Axiom ha reescrito esta prueba en Lean, un asistente de prueba: un lenguaje donde cada definición y cada paso lógico están escritos con la suficiente precisión para que un programa los controle. El sitio del proyecto muestra 43,1 millones de líneas de Lean y 2,05 millones de declaraciones.

Cómo se puso a contribución la IA

El relato de Axiom es sobre todo el de una organización. El proyecto arranca el 1 de octubre de 2026 con un mapa de prueba extraído de la literatura y del código Lean ya existente, dividido en 108 hitos y unas 380 tareas. Desde el 2 de octubre, enjambres de varias decenas de agentes AxiomProver, utilizando una mezcla cambiante de modelos, reclaman tareas mediante tickets de GitHub y rinden cuentas en Slack. Agentes « jefes » descomponen los argumentos difíciles y verifican los enunciados; otros buscan resultados existentes o escriben las pruebas.

Axiom no oculta los tropiezos. Hitos aparentemente sencillos escondían enormes prerrequisitos que los agentes habían supuesto en lugar de demostrarlos: se eliminaron decenas de miles de líneas. El tiempo de recompilación también se convirtió en un cuello de botella, resuelto por un sistema de caché compartido entre máquinas. Los humanos seguían en el centro: matemáticos para los obstáculos de fondo, ingenieros para hacer funcionar el sistema.

Lo que encontró la máquina

Formalizar obliga a explicitar lo que un lector humano completa por sí mismo. Según Axiom, la mayoría de los problemas señalados eran menores (erratas, tablas erróneas, hipótesis olvidadas), pero 34 discrepancias notables con la literatura tuvieron que resolverse. La más seria afecta al teorema de los grupos no equilibrados, en la versión de John Walter de 1986: los agentes encontraron contraejemplos a un paso del razonamiento, sin por ello refutar el teorema mismo. Con la ayuda de Richard Lyons y Ronald Solomon, dos especialistas históricos de la clasificación, se construyó otra vía a partir de trabajos de Solomon de 1976. Axiom la presenta como un nuevo resultado de teoría de grupos, descrito en un artículo que acompaña la publicación.

Axiom promete publicar la lista completa de erratas con un comité de especialistas. Mientras no esté en línea, el número total de errores señalados sigue siendo inverificable.

Los límites a tener en cuenta

Lean controla las deducciones, no el sentido del enunciado: todavía hace falta que humanos verifiquen que el teorema final y sus definiciones dicen bien lo que dice la clasificación. Axiom lo reconoce en su texto. En el momento de escribir, ninguna verificación independiente completa ha sido publicada y no hemos recompilado nosotros mismos el repositorio. La formalización tampoco parte de cero: integra unas 1,2 millones de líneas del proyecto Qiuzhen-CFSG y se apoya en la biblioteca Mathlib.

Este anuncio llega al día siguiente de los resultados matemáticos reivindicados por OpenAI, que hemos presentado aquí. El enfoque es diferente: OpenAI dice haber encontrado resultados nuevos, Axiom dice haber verificado mecánicamente un resultado conocido y haber corregido partes de él.