La Clasificación de Grupos Simples Finitos (CFSG) se considera uno de los logros colectivos más significativos en la historia de las matemáticas. El teorema establece que cada grupo simple finito —los bloques de construcción fundamentales de la teoría de grupos finitos— cae en una de varias categorías: grupos cíclicos de orden primo, grupos alternantes, grupos de tipo Lie o uno de los 26 grupos 'esporádicos'. Debido a que la prueba original fue una empresa masiva que abarcó décadas e involucró a aproximadamente 100 matemáticos a lo largo de miles de páginas de artículos en revistas, ha sido durante mucho tiempo un candidato para la verificación formal con el fin de asegurar su integridad lógica absoluta.
Esta imagen representa el proyecto general de formalizar la Clasificación de Grupos Simples Finitos utilizando el demostrador de teoremas Lean.
Investigadores de AxiomMath han producido ahora una formalización completa de la CFSG en Lean, un lenguaje de programación funcional y demostrador de teoremas interactivo utilizado para verificar pruebas matemáticas. El proyecto sigue la prueba de 'primera generación' de la CFSG, asegurando que cada paso lógico sea comprobado por el núcleo de Lean. La formalización es 'libre de disculpas', lo que significa que no depende de marcadores de posición para pasos no probados. El equipo utilizó la declaración de la CFSG del proyecto TauCeti como base y construyó la prueba sobre Mathlib y TauCeti, utilizando axiomas estándar como `Classical.choice`, `propext` y `Quot.sound`.
Uno de los resultados más significativos de este proyecto de formalización fue el descubrimiento de un error técnico en la literatura existente. Mientras verificaban la prueba de primera generación, el equipo identificó un contraejemplo a una afirmación de clausura utilizada en una ruta publicada hacia el Teorema del Grupo Desequilibrado. Para resolver esto, el equipo desarrolló un argumento alternativo para el caso de grupos simples basado en la teoría de componentes 2-maximales de Solomon de 1976. Este descubrimiento resalta la utilidad de la verificación formal: al traducir pruebas escritas por humanos en código verificable por máquinas, los investigadores pueden descubrir brechas sutiles en obras matemáticas complejas de múltiples autores que, de otro modo, podrían permanecer sin detectar durante años. El proyecto consta actualmente de más de 43 millones de líneas de código en Lean e incluye un mapa de prueba interactivo para visualizar las dependencias entre varios artículos y libros en el corpus.
Esta imagen se relaciona con la escala masiva del proyecto y el repositorio donde se aloja la formalización.