Axiom dice haber verificado por computador, con agentes de IA y en 24 días, la demostración de 15.000 páginas de los grupos simples finitos

La startup Axiom publicó el 26 de octubre una formalización completa en Lean de la Clasificación de los Grupos Simples Finitos, una demostración de unas 15.000 páginas repartidas en más de 500 artículos. Enjambres de agentes de IA escribieron unos 43,1 millones de líneas en 24 días y hallaron 34 desviaciones relevantes respecto de lo publicado, casi todas menores. Aún no hay una revisión independiente.