La clasificación de los grupos simples finitos, formalizada en Lean
Classification of Finite Simple Groups Formalized in Lean
La clasificación de los grupos simples finitos, una de las mayores gestas colectivas de las matemáticas, ha sido formalizada por completo en Lean. El proyecto, de 43,1 millones de líneas de código, sigue la prueba de primera generación y verifica cada paso lógico con el kernel de Lean. Durante el proceso, el equipo detectó un fallo en un argumento publicado del Teorema de los Grupos Desbalanceados y propuso una ruta alternativa.
En el camino, encontramos un problema en un argumento publicado para el Teorema de los Grupos Desbalanceados.