Axiom afirma que agentes de IA formalizaron la Clasificación de los grupos simples finitos en Lean

Axiom, una empresa de matemáticas con IA, anunció en X una formalización automática completa en Lean de la Clasificación de los grupos simples finitos, un resultado que denomina la «tabla periódica de la simetría». Describe la demostración original como de unas 15.000 páginas, escrita por más de 100 matemáticos a lo largo de varias generaciones, y la califica como la demostración matemática más extensa de la historia verificada por computadora.

Según el repositorio de código abierto de Axiom, enjambres de agentes de IA generaron unos 43,1 millones de líneas de Lean en 24 días, abarcaron 715 artículos y libros y señalaron 34 discrepancias con el registro publicado. Una publicación de la cuenta de noticias de IA TestingCatalog añade que los agentes dividieron el trabajo como equipos de software y escribieron código más rápido de lo que Lean podía verificarlo.

Estas cifras son la versión de Axiom; el anuncio no incluye una revisión independiente de la formalización. La publicación tenía unos 6.200 «me gusta» en X al 28 de octubre.