En 7 meses, supera el trabajo de 15 matemáticos en 6 años: IA escribe millones de líneas de código para verificar un colosal proyecto de demostración matemática
**FormaTheoria: IA ayuda a formalizar el colosal teorema de clasificación de grupos finitos simples (CFSG)**
El teorema de clasificación de grupos finitos simples (CFSG), una de las demostraciones más extensas y fundamentales de las matemáticas modernas, abarca decenas de miles de páginas dispersas en cientos de artículos. Verificar su integridad manualmente es casi imposible. Un equipo liderado por la Universidad Tsinghua y el Centro de Ciencias Matemáticas Yau ha desarrollado **FormaTheoria**, un flujo de trabajo asistido por IA para abordar este desafío.
Este sistema permite que la IA analice literatura matemática original, identifique dependencias, integre conocimientos y construya demostraciones formales que luego son verificadas paso a paso por el asistente de pruebas Lean. Superando dificultades como definiciones inconsistentes entre textos y errores tipográficos en las fuentes, FormaTheoria implementa un riguroso proceso de traducción y revisión independiente.
Entre enero y agosto de 2026, en solo **7 meses**, el sistema logró formalizar en Lean cuatro teoremas clave interconectados del CFSG (Feit-Thompson, Glauberman Z*, Brauer-Suzuki, Bender-Suzuki), generando una red de **más de 994,000 líneas de código** y **186,187 dependencias**. Esto supera significativamente el trabajo previo de formalización manual del teorema de Feit-Thompson, que requirió años. Además, el proceso sacó a la luz y corrigió ambigüedades y errores sutiles en las fuentes originales.
Este hito demuestra el potencial de la IA para participar en la construcción sistemática de conocimiento matemático a gran escala, colaborando con humanos que guían la investigación y realizan juicios clave, mientras los sistemas formales garantizan la verificabilidad de cada paso. FormaTheoria avanza hacia la verificación completa del CFSG, creando una infraestructura de conocimiento reutilizable y trazable para futuras investigaciones.
marsbitHace 24 min(s)
