Axiom Math ha publicado la primera demostración completa y verificada por ordenador de la clasificación de los grupos finitos simples, considerada la prueba más larga de la historia de las matemáticas. Lo ha hecho en 24 días, con enjambres de decenas de agentes de IA coordinados por ingenieros y matemáticos, y el resultado son unos 43,1 millones de líneas de código en Lean. Lo cuenta en su blog de investigación del 26 de octubre.
La demostración original ocupa unas 15.000 páginas repartidas en más de 500 artículos de unos 100 matemáticos, y por eso se la conoce como "el teorema enorme". Por el camino, los agentes encontraron 34 desviaciones relevantes respecto a lo publicado y produjeron un resultado nuevo de teoría de grupos.
Puntos clave
- Qué: la clasificación de los grupos finitos simples (CFSG, por sus siglas en inglés), formalizada entera en Lean, un lenguaje en el que un ordenador comprueba cada paso de una demostración.
- Cuánto: unos 43,1 millones de líneas de Lean en 24 días, divididas en 108 hitos y unas 380 tareas.
- Qué encontraron: erratas, tablas mal y, en 34 casos, desviaciones serias. La más grave, en la demostración del teorema del grupo no equilibrado (UGT).
- Novedad: AxiomProver demostró un teorema nuevo ("preservación de cimas simples") para reparar ese hueco.
- Supervisión: Richard Lyons y Ronald Solomon, dos de los matemáticos que trabajaron en la clasificación original, asesoraron el proyecto.
Qué es el teorema enorme
Un grupo, en matemáticas, describe simetrías. Un cubo tiene 24 formas de girarlo para que quede igual que antes, y esas 24 rotaciones forman un grupo. Los grupos finitos se pueden descomponer en piezas que ya no se pueden partir más, los grupos finitos simples, y la clasificación es la lista completa de esas piezas. Axiom la llama una tabla periódica de la simetría.
La lista tiene familias infinitas y 26 grupos "esporádicos" que no encajan en ninguna. El mayor es el Monstruo, con unos 8 × 10^53 elementos. Lo difícil de la clasificación es demostrar que no falta ninguno.
La historia del teorema es larga. Daniel Gorenstein anunció en 1983 que la clasificación estaba completa, y no lo estaba: un caso dependía de un manuscrito sin terminar y el hueco no se cerró hasta 2004, con un tratamiento de 1.221 páginas de Michael Aschbacher y Stephen Smith. Hubo correcciones después, en 2008. Desde finales de los ochenta hay en marcha una "segunda generación" de la prueba, más ordenada, de la que han salido diez volúmenes y se esperan al menos doce. El propio Aschbacher escribió en 2005 que es imposible escribir un argumento tan largo y complicado sin errores.
Cómo trabajó el enjambre
Axiom abrió un canal de Slack el 1 de octubre para coordinar el proyecto y el primer enjambre arrancó el día 2. Partían de trabajo previo en Lean (incluidas unas 1,2 millones de líneas de otro proyecto, Qiuzhen-CFSG) y de un mapa de la demostración que habían montado a partir de la literatura.
Ese mapa dividía el trabajo en 108 hitos y unas 380 tareas. Un agente cogía una tarea por un issue de GitHub, buscaba los argumentos en los artículos, los traducía a Lean y, si necesitaba algo que aún no estaba formalizado, se lo encargaba a otro agente. Había agentes jefe que partían los argumentos difíciles y revisaban enunciados, otros que buscaban resultados ya existentes y otros que solo escribían pruebas. Los matemáticos humanos investigaban los obstáculos y los ingenieros mantenían el sistema funcionando.
No fue lineal. Algunos hitos que parecían fáciles escondían requisitos enormes que los agentes habían dado por supuestos sin demostrarlos, y Axiom tuvo que borrar decenas de miles de líneas y replantear partes. El 13 de octubre solo se cerró un hito. Hubo que replanificar, partiendo lo que faltaba en teoremas más pequeños y bien enunciados.
El otro cuello de botella fue de ingeniería. Los agentes producían pruebas más rápido de lo que Lean podía comprobarlas, y cambiar un resultado compartido obligaba a recomprobar todo lo que dependía de él. Axiom montó un sistema para repartir resultados ya compilados entre máquinas y lanzar comprobaciones en paralelo, y sacó los cálculos más caros a certificados que se verifican aparte. Según la empresa, eso aceleró la verificación en órdenes de magnitud.
El 10 de octubre apareció un mensaje en el canal: habían demostrado que el Monstruo es simple.
Lo que encontraron las máquinas
Formalizar obliga a escribir todo lo que un matemático humano rellena de cabeza. La mayoría de avisos de los agentes eran inocuos: erratas, tablas con errores o hipótesis que se daban por sabidas. Pero algunos eran matemática de verdad.
En los volúmenes de Aschbacher y Smith, un lema afirmaba que dos cantidades eran iguales. Los agentes encontraron un contraejemplo con el grupo SL₂(5) en el que una valía 1 y la otra tenía que valer 2. Cambiar la igualdad por una desigualdad arreglaba el lema, pero obligaba a revisar argumentos posteriores que se apoyaban en ella.
El caso más serio fue el UGT, un teorema que permite identificar un grupo entero a partir de información sobre sus subgrupos. La prueba de John Walter de 1986 usaba una afirmación que los agentes refutaron con contraejemplos concretos. El objetivo del teorema seguía en pie, pero el paso quedaba sin justificar. Con las ideas de un trabajo de Solomon de 1976, AxiomProver produjo y formalizó un argumento alternativo que incluye un teorema nuevo. Axiom publicará la lista de erratas para la comunidad de teoría de grupos.
Lo que hacen las personas
Axiom insiste en que la parte humana fue imprescindible. Los matemáticos investigaron los avisos más graves, y saber que existía una ruta alternativa (o que un arreglo natural era circular) cambió la dirección del proyecto más de una vez.
También hay un límite que la propia empresa explica bien. Lean comprueba las deducciones, pero son las personas las que tienen que revisar que el enunciado final dice de verdad lo que se quería demostrar. Un resultado probado con una hipótesis de más puede pasar el compilador y dejar el trabajo a medias.
Esto llega tres semanas después de que OpenAI publicara 722 manuscritos de matemáticas escritos por su IA, también apoyados en Lean, y después de la carta de 25 medallas Fields quejándose de cómo se anuncian estos resultados. Axiom ha optado por enseñarlo todo: la prueba completa, el grafo de dependencias y el artículo con la reparación.
Por qué importa
Lo útil de este proyecto para cualquiera que no sea matemático es el método. Un trabajo gigante dividido en 380 tareas, agentes que se reparten el trabajo y se delegan lo que les falta, un verificador automático que no deja pasar nada sin comprobar y personas revisando solo lo que de verdad necesita criterio.
Y la lección que más se va a repetir fuera de las matemáticas: los agentes daban por supuestas cosas que no estaban demostradas, y hubo que tirar decenas de miles de líneas. Si en tu empresa pones varios agentes a trabajar en paralelo, sin un verificador que compruebe cada pieza, los supuestos se acumulan sin que nadie los vea.
Fuente original: axiommath.ai
Relacionado
