La Clasificación de Grupos Finitos Simples (CFSG) es uno de los proyectos de demostración más vastos en las matemáticas modernas.
Esta demostración, completada en relevo por cientos de matemáticos a lo largo de décadas, se encuentra dispersa en cientos de artículos y monografías, con un volumen total cercano a veinte mil páginas, una magnitud que ya sobrepasa enormemente los límites de lo que un individuo o incluso un solo equipo podría verificar por completo.
En este contexto, la introducción de la IA como asistente para la verificación formal a gran escala se convierte en un nuevo camino que debe explorarse.
Para impulsar el desarrollo de la IA para las matemáticas, bajo el impulso del Profesor Shing-Tung Yau, un equipo de investigación compuesto por estudiantes de la Clase de Liderazgo de la Escuela Qiuzhen de la Universidad de Tsinghua, junto con investigadores del Centro de Ciencias Matemáticas Yau, el Instituto de Investigación de Industrias Inteligentes y la Universidad de Warwick, propuso FormaTheoria – un flujo de trabajo de asistencia por IA para la investigación matemática: dejar que la IA parta de la literatura matemática original, organice automáticamente las relaciones de dependencia, integre el sistema de conocimiento y construya demostraciones formales, para finalmente ser verificadas paso a paso por el asistente de pruebas Lean.
Hasta agosto de 2026, FormaTheoria ya ha completado la formalización en Lean de cuatro teoremas clave, generando más de 994,000 líneas de teoría matemática codificada e interconectada. Aunque aún queda un largo camino para la verificación completa de la CFSG, este logro ya representa un hito importante hacia ese objetivo final.
La CFSG proporciona la base para una gran cantidad de resultados matemáticos importantes
La "Clasificación de Grupos Finitos Simples" suena muy abstracta. En términos sencillos, es como una "lista de piezas básicas" sobre simetrías finitas: cualquier estructura simétrica finita compleja puede descomponerse en capas hasta obtener un conjunto de unidades básicas que ya no se pueden dividir más; y el papel de la CFSG es precisamente decirle a los matemáticos cuáles son esas unidades básicas.
Normalmente, la investigación matemática primero descompone un problema complejo en estas unidades básicas, y luego lo procesa clase por clase según la lista completa proporcionada por la CFSG. Por lo tanto, la CFSG se convierte en una infraestructura que otras demostraciones pueden invocar en cualquier momento. Si esta "infraestructura" oculta fallas, una gran cantidad de resultados posteriores basados en sus conclusiones podrían verse afectados.
Algunas revisiones especializadas proporcionan pruebas cuantitativas de la aplicación de la CFSG. La Sociedad Americana de Matemáticas publicó en 2018 la monografía de Stephen D. Smith "Applying the Classification of Finite Simple Groups: A User’s Guide", que con 231 páginas y 10 capítulos, sistematiza los escenarios de aplicación de la CFSG. Los dos últimos capítulos de su índice público enumeran 14 temas de aplicación numerados, incluyendo gráficas distancia-transitivas, la conjetura de Frobenius, algoritmos para grupos de permutaciones, crecimiento de subgrupos en grupos finitamente generados, extensiones de cuerpos, recubrimientos de superficies de Riemann, el problema de Waring en teoría de grupos, gráficas expansoras y grupos aproximados, entre otros.
El valor aplicado de la CFSG también ha recibido reconocimiento al más alto nivel de la comunidad matemática internacional. En el Congreso Internacional de Matemáticos de 2014, se invitó a Robert Guralnick, ganador del Premio Cole de Álgebra 2018 de la AMS, a dar una conferencia titulada "Applications of the Classification of Finite Simple Groups".
Estas aplicaciones incluyen resultados importantes de gran impacto académico. La CFSG es un eslabón clave en la cadena de demostración completa del Problema de Burnside Restringido, por cuya resolución Efim Zelmanov recibió la Medalla Fields en 1994. La monografía de Smith también incluye entre las direcciones de aplicación importantes de la CFSG el problema de Waring sobre grupos simples finitos y las gráficas expansoras, con trabajos representativos publicados en *Annals of Mathematics* (problema de Waring; diámetro de grupos simples finitos y sus aplicaciones). Estos ejemplos muestran que la CFSG ya sustenta una serie de trabajos importantes que han obtenido premios académicos de primer nivel y han llegado a las revistas matemáticas más prestigiosas.
En este sentido, la CFSG se ha convertido en un sistema base que se utiliza repetidamente. A medida que se acumulan más resultados posteriores, verificar su corrección y capacidad de revisión se vuelve cada vez más crucial. La verificación por máquina, rastreable y reproducible, de la CFSG adquiere un significado que va más allá de la teoría de grupos en sí.
Sin embargo, la dificultad radica en que las demostraciones de este sistema base provienen de diferentes épocas, autores y fuentes, utilizando símbolos, definiciones y condiciones por defecto que a menudo no son consistentes; una sola cita puede incluso apuntar a toda otra literatura. Históricamente, una brecha importante en la demostración de la clasificación no se llenó hasta más de veinte años después, con una monografía en dos volúmenes que sumaba 1220 páginas. FormaTheoria no solo necesita verificar paso a paso el razonamiento individual, sino también comprobar que las definiciones, condiciones y citas entre cientos de documentos puedan conectarse sin interrupciones, formando finalmente una cadena de demostración continua.
Cómo la IA avanza en proyectos de demostración a gran escala
Muchos sistemas de IA matemática se enfrentan a un problema ya preparado, incluyendo el enunciado, las definiciones y las herramientas listas; la IA solo se encarga de encontrar la demostración. Pero FormaTheoria es diferente: primero debe reconstruir los fundamentos matemáticos detrás del problema a partir de literatura dispersa, y luego completar la demostración. Este trabajo enfrenta principalmente cuatro dificultades:
Primero, el sistema no sabe de antemano cuánta información necesita consultar.
Una cita puede llevar a otro artículo, que a su vez puede llevar a más trabajos previos. Inicialmente, el proyecto solo tenía 3 fuentes principales, pero durante la demostración se descubrieron 12 fuentes adicionales; el material complementario posterior representó aproximadamente el 65.6% de todas las páginas consultadas. El método de FormaTheoria es: una vez que detecta que falta un teorema previo, pausa la demostración actual, busca y formaliza esa dependencia, y luego vuelve a la tarea original para continuar. Los resultados ya verificados se almacenan en una base de conocimiento unificada, disponible para ser reutilizados en demostraciones posteriores.
Segundo, es difícil conectar directamente diferentes fuentes literarias.
Diferentes autores usan definiciones, símbolos y condiciones por defecto distintas. Dos definiciones pueden ser matemáticamente equivalentes, pero una vez escritas en código Lean, pueden ser incompatibles. FormaTheoria compara repetidamente el texto original y el código existente para establecer las relaciones de conversión necesarias. Simultáneamente, el sistema protege los enunciados matemáticos ya verificados y verifica si cada corrección afecta a las demostraciones posteriores. De esta manera, múltiples obras y artículos independientes pueden integrarse gradualmente en un mismo marco teórico.
Tercero, el código puede pasar la verificación y aún así malinterpretar el original.
Lean solo verifica si la lógica de la demostración es consistente y si la conclusión se deriva de las premisas, pero no juzga si esa conclusión es fiel al texto original. La IA podría omitir una condición, confundir "para todo" con "existe", o incluso alterar erróneamente la conclusión. Para ello, FormaTheoria establece un control de revisión independiente: el componente de traducción escribe primero el enunciado en Lean, y el componente de revisión lo verifica punto por punto contra el original. De las 14 secciones literarias analizadas en el artículo, las traducciones iniciales de 11 secciones fueron devueltas para su modificación. Este mecanismo de revisión independiente se convierte así en una segunda "seguridad" además de la verificación automática.
Cuarto, la literatura original en sí misma también puede tener problemas.
En literatura antigua pueden aparecer errores tipográficos, condiciones faltantes o formulaciones ambiguas. FormaTheoria conserva la página original, y cuando una demostración posterior encuentra una contradicción, retrocede para investigar. Si la literatura respalda una corrección, el sistema agrega la condición o establece una relación de compatibilidad; si la evidencia es insuficiente, el sistema registra el problema y lo deja en manos de profesionales matemáticos.
Además, este proyecto requiere que la IA mantenga un ritmo a lo largo de un ciclo prolongado. Un solo diálogo no puede contener la tarea completa. Para ello, FormaTheoria utiliza un "mapa de demostración" continuamente actualizado para gestionar el progreso: los objetivos más arduos se dividen en lemas auxiliares más pequeños, los resultados exitosos se integran gradualmente en el teorema principal, y las rutas fallidas también se registran para evitar que el sistema caiga repetidamente en el mismo callejón sin salida.
En cuanto a la estrategia de paralelización, el proyecto tiene un diseño especial. Las tareas independientes pueden avanzar simultáneamente; si múltiples tareas encuentran el mismo resultado previo, el sistema lo completa una sola vez y permite que otras tareas lo reutilicen. El contenido matemático público que podría afectar a todo el sistema se modifica secuencialmente para evitar conflictos. Los experimentos de control del artículo muestran que este enfoque paralelo sensible a las dependencias logró una aceleración de 4.2 veces en las tareas probadas.
Así, FormaTheoria forma una cadena de trabajo completa: buscar literatura, completar dependencias, traducir el original, construir demostraciones, verificar por máquina, revisión independiente, coordinar conflictos y dejar los problemas dudosos en manos de profesionales matemáticos. Cada paso tiene responsabilidades claras y está basado en evidencia. Este diseño responde precisamente a las dificultades prácticas que surgen en proyectos de demostración a gran escala, empoderando a la IA para conectar gradualmente literatura matemática dispersa en un sistema teórico verificable, rastreable y sosteniblemente extensible.
△
Siete meses, cuatro teoremas clave, casi un millón de líneas de código verificable
El 22 de enero de 2026, FormaTheoria realizó su primer envío de código. Hasta el 2 de agosto de 2026, el proyecto ya había establecido una cadena teórica clave que se extiende hasta el teorema de Bender-Suzuki, habiendo completado en el camino las demostraciones del teorema de Feit-Thompson sobre grupos de orden impar, el teorema Z* de Glauberman y el teorema de Brauer-Suzuki.
Estos cuatro teoremas no están aislados; forman una ruta importante interconectada dentro de la clasificación de grupos finitos simples, donde la demostración de un teorema posterior a menudo se basa en la vasta base matemática establecida por los anteriores.
El estado del proyecto al completar estas demostraciones incluye:
- Más de 994,000 líneas de código Lean ;
- Más de 850 archivos de código ;
- El sistema consultó 15 libros y artículos, con un total de 1037 páginas, de las cuales aproximadamente dos tercios se descubrieron gradualmente durante el avance de las demostraciones.
Por supuesto, el número de líneas de código solo muestra un aspecto del volumen del proyecto. Si se traza retrospectivamente desde el teorema de Bender-Suzuki como punto final, el proyecto ha formado una red de demostraciones que contiene 30,298 declaraciones matemáticas y 186,187 relaciones de dependencia, con una cadena de dependencia más larga de 458 niveles. Si se incluye el contenido relevante de la biblioteca base de Lean, esta red se expande a 74,922 declaraciones y más de 1.44 millones de relaciones de dependencia. Puede decirse que detrás de las casi un millón de líneas de código hay una red de demostraciones intrincada y estrechamente conectada. Esta investigación indica que los agentes de IA ya pueden, bajo la acción conjunta de la verificación automática y la revisión por capas, impulsar continuamente grandes proyectos matemáticos de largo alcance.
El proceso de ejecución real del proyecto también tiene características de muy largo plazo. La ejecución más larga de un agente registrada en el artículo duró 9.17 días, durante los cuales el sistema comprimió y organizó la información acumulada 606 veces, manteniendo siempre el objetivo de demostración actual, los resultados ya completados y los problemas pendientes. Estos datos muestran que el proyecto gestiona una red de demostración de muy largo alcance en constante evolución, que una sola generación o un solo diálogo no pueden cubrir.
Anteriormente, la formalización matemática a gran escala dependía en gran medida de la inversión manual, requiriendo típicamente la colaboración continua de varios investigadores durante años. Una referencia histórica para comparar: la versión formalizada previa del teorema de Feit-Thompson en Rocq tomó a unas 15 personas seis años en completarse. FormaTheoria completó todo el contenido de ese proyecto manual en siete meses, y además extendió el trabajo de formalización a otros teoremas clave. Siete meses sigue siendo un ciclo de ejecución extremadamente largo para una tarea de agente de IA, pero en comparación con la formalización manual tradicional, la intervención de la IA acorta significativamente la escala temporal del proyecto.
△
La formalización hace que los problemas ocultos en la literatura emerjan uno por uno
La literatura matemática suele estar dirigida a investigadores familiarizados con el campo. Por lo tanto, los autores a menudo omiten condiciones ya mencionadas anteriormente, o asumen que el lector puede reconocer la equivalencia entre diferentes definiciones. Algunos pequeños errores tipográficos o de símbolos a menudo se pasan por alto o se corrigen naturalmente durante la lectura humana. Pero FormaTheoria es diferente: al traducir la literatura línea por línea a código Lean, cada definición, cada condición y cada paso del razonamiento debe escribirse de manera clara y sin ambigüedades. Es precisamente este requisito estricto de verificación línea por línea lo que hace que los problemas originalmente ocultos en la literatura se vuelvan evidentes.
El artículo registra en detalle varios problemas literarios descubiertos por el proyecto, incluyendo definiciones inconsistentes para el mismo concepto en diferentes fuentes, teoremas que omiten condiciones necesarias, condiciones de divisibilidad colocadas incorrectamente, e incluso errores en subíndices dentro de demostraciones. Algunos de estos problemas pueden corregirse automáticamente según el contexto de la literatura; los problemas con evidencia insuficiente se dejan a matemáticos para una evaluación posterior.
Un caso típico proviene de dos fuentes sobre el teorema de orden impar. Ambas definen "subgrupo máximo de tipo I", pero la diferencia es: una requiere que cierta propiedad se cumpla para "cada estructura complementaria"; la otra solo requiere que "exista una estructura complementaria" que cumpla la propiedad. Formalmente, la primera es claramente más fuerte que la segunda, por lo que las dos definiciones no pueden conectarse directamente. FormaTheoria identificó astutamente esta diferencia durante el proceso de formalización, y luego, utilizando el teorema de Schur-Zassenhaus, demostró que ambas definiciones son en realidad equivalentes en este contexto, construyendo así con éxito un puente entre las dos fuentes.
Otro caso proviene de un lema de Peterfalvi. El enunciado formal de este lema omitía la condición previa de que "el orden de cierto grupo es impar", sin embargo, la demostración posterior realmente depende de esta condición. Aunque en la aplicación posterior del lema, el contexto anterior ya garantizaba esta condición y el argumento general no se interrumpía, Lean no completará automáticamente esta información de fondo. FormaTheoria, tras rastrear la ruta de demostración y las posiciones de uso de este lema, agregó automáticamente la condición omitida al enunciado del teorema, haciendo que toda la cadena de formalización sea más completa y confiable.
△
El proyecto también descubrió errores literarios más directos. Una definición escribió el objeto H donde debía ser M, y dos fuentes de referencia conservaban el mismo error. Un teorema de Huppert colocó el factor d en una condición de divisibilidad incorrecta; el sistema encontró un contraejemplo y detuvo la demostración, dejando el problema para verificación por matemáticos. La condición correcta fue confirmada manualmente. Un fragmento de demostración de Higman también numeró un conjunto de vectores base de u0 a um, cuando el rango correcto debería ser hasta um−1; este error de subíndice fue identificado y corregido automáticamente por el sistema durante el proceso de demostración.
Estos casos reflejan otro valor importante de la verificación por máquina para grandes proyectos matemáticos. FormaTheoria, al construir demostraciones formales, también realiza una revisión de grano fino de la literatura original: registra dónde aparecen los problemas, qué condiciones necesita la demostración posterior, en qué literatura se basa la corrección y si la modificación afecta otros resultados. Para la CFSG, formada por cientos de fuentes interconectadas, este mecanismo de revisión rastreable puede transformar esos detalles que antes dependían de la experiencia del lector para completarse, en bases matemáticas explícitamente verificables.
Perspectivas futuras
FormaTheoria aún no ha completado la formalización integral de la Clasificación de Grupos Finitos Simples, y queda un largo camino hacia el objetivo final. El proyecto está avanzando rápidamente, continuando hacia la formalización completa de uno de los proyectos de demostración más grandes en las matemáticas modernas. Los resultados actuales muestran que la IA ya puede mantener y expandir entornos matemáticos a gran escala durante meses, rastrear relaciones de dependencia complejas a través de múltiples fuentes y, bajo verificación estricta, construir sistemas teóricos interconectados y de volumen considerable. Así, los límites de capacidad de la IA comienzan a expandirse desde la resolución de problemas matemáticos aislados hasta la participación en la construcción sistemática del conocimiento matemático.
Este trabajo también formará una infraestructura matemática sosteniblemente extensible y reutilizable. La literatura tradicional solo puede decirle al lector "dónde está escrita la demostración"; el código formalizado va más allá, registrando "de qué depende cada conclusión", "cómo se conectan diferentes fuentes" y "qué problemas se han corregido", y organizando las definiciones, lemas y demostraciones ya verificados en módulos de conocimiento listos para ser invocados directamente por investigaciones futuras. Una vez que se agreguen herramientas de explicación, búsqueda y visualización, esta red de conocimiento podría ayudar a los investigadores a comprender más rápidamente la estructura general de la CFSG, reutilizar resultados existentes e incluso proporcionar un fuerte apoyo para que los matemáticos humanos exploren nuevas conexiones y descubran nuevos teoremas.
El equipo del proyecto FormaTheoria espera explorar un modo de colaboración humano-máquina para la era de la IA: los humanos se encargan de identificar problemas dignos de estudio y tomar juicios clave, la IA asume la búsqueda y derivación a gran escala, y el sistema formal garantiza que cada paso aceptado pueda ser reexaminado. Cuando una demostración es tan vasta que ningún individuo puede verificarla desde el principio, esta combinación de los tres elementos podría convertirse en un camino completamente nuevo para que la humanidad gestione el conocimiento matemático a una escala sobrehumana.
Nota: El estado del proyecto y los resultados cuantitativos mencionados corresponden a la instantánea de agosto de 2026 descrita en el artículo.
Artículo: https://arxiv.org/abs/2608.10894
Código: https://github.com/Qiuzhen-CFSG/CFSG
Este artículo proviene de la cuenta pública de WeChat "Quantum Bit", autores: Equipo FormaTheoria
