Axiom Math informó el 26 de octubre que había completado lo que describe como la primera prueba completa de la Clasificación de los Grupos Simples Finitos verificada por ordenador en Lean.
En el anuncio de Axiom Math, la empresa afirma que el proyecto formalizó la prueba CFSG de primera generación y la redujo a pasos que Lean podía verificar mecánicamente. Axiom también indica que el trabajo duró 24 días, utilizó decenas de agentes de IA y generó aproximadamente 43.1 millones de líneas de código Lean.
La formalización hizo más que reproducir la literatura. Axiom afirma que detectó 34 discrepancias relevantes respecto a argumentos publicados y señaló un problema en una ruta publicada hacia el Teorema de los Grupos Desequilibrados. La empresa planea publicar una lista de erratas más extensa para matemáticos.
Para quienes crean automatizaciones, la parte interesante es menos el teorema principal que el modelo operativo: dividir un problema con muchas dependencias en subproblemas trazables y mantener un verificador en el ciclo para que una salida plausible no se confunda con un resultado terminado. Este patrón es relevante allí donde los agentes necesitan demostrar cobertura y corrección, no solo producir texto que parezca completo.