Axiom afirma haber completado en Lean la primera prueba comprobada por ordenador de la clasificación de los grupos simples finitos. El corpus original ocupa unas 15.000 páginas repartidas en más de 500 artículos de alrededor de cien matemáticos. El equipo produjo 43,1 millones de líneas en 24 días mediante decenas de agentes de IA dirigidos por matemáticos e ingenieros.
Lean comprueba que cada paso se sigue de definiciones, hipótesis y teoremas previos dentro del sistema formal. Eso ofrece una garantía mucho más precisa que una lectura informal de miles de páginas. No responde por sí solo a otra pregunta: si las definiciones formalizadas representan exactamente la clasificación que la comunidad matemática pretende demostrar.
La escala no es solo contar líneas
Axiom dividió el trabajo en 108 hitos y unas 380 tareas. Los agentes buscaban resultados existentes, escribían pruebas y delegaban prerrequisitos; los humanos resolvían obstáculos matemáticos y revisaban la integración. El propio relato reconoce que se eliminaron decenas de miles de líneas cuando una parte se apoyó en supuestos adicionales sin justificar.
La formalización localizó 34 desviaciones destacables respecto al registro publicado, además de erratas menores y hipótesis omitidas. La más importante afectaba al teorema de grupos desequilibrados. Axiom dice haber consultado a especialistas y prepara una lista detallada de correcciones. Hasta que esa lista y el corpus sean examinados fuera del equipo, conviene hablar de una formalización comprobada por Lean publicada por su creador, no de consenso independiente cerrado.
Tres niveles de confianza distintos
| Pregunta | Qué aporta Lean | Qué sigue necesitando personas |
|---|---|---|
| ¿Compila la cadena lógica? | Comprueba tipos, hipótesis y pasos | Auditar el entorno de confianza |
| ¿Es el teorema correcto? | Verifica el enunciado formal | Compararlo con la intención matemática |
| ¿Es útil la nueva ruta? | Permite reproducir dependencias | Entender, simplificar y revisar decisiones |
El antecedente explica por qué esta prueba es difícil. El anuncio de 1983 resultó prematuro y un caso quedó abierto hasta 2004; otra laguna se corrigió en 2008. La formalización no borra esa historia: la convierte en dependencias explícitas que dejan de avanzar cuando falta un argumento.
El resultado muestra una aportación concreta de los agentes: coordinación masiva de tareas formales con un verificador determinista al final. No demuestra que cualquier descubrimiento matemático generado por un modelo sea fiable, ni que 24 días sustituyan el trabajo acumulado en el corpus que sirvió de base. La afirmación fuerte debe sostenerse en los archivos publicables, sus hashes, el entorno Lean y revisión externa del enunciado.
Transparencia: artículo elaborado con asistencia de IA a partir del informe textual de Axiom, que enlaza material formal. Texploto no compiló las 43,1 millones de líneas ni verificó de forma independiente la equivalencia matemática.
