Lunes 2 de noviembre de 2026 ·
Axiom Math formaliza en Lean la clasificación de grupos simples finitos con agentes de IA
Axiom Math anunció el 26 de octubre de 2026 la formalización completa del teorema de clasificación de grupos simples finitos (CFSG), conocido como el 'Teorema enorme', usando un enjambre de agentes de IA. La prueba original ocupa más de 15.000 páginas repartidas en más de 500 artículos, y la versión verificada se cifra en unos 41,3 millones de líneas de código Lean. Los agentes generaron 43,1 millones de líneas en 24 días.
Qué significa
La demostración más larga de las matemáticas queda verificada por ordenador, así que los matemáticos ya no dependen solo de la revisión humana de cientos de artículos. Es un ejemplo de cómo la IA puede comprobar pruebas que ninguna persona podría revisar entera.
Fuentes originales
Resumen de Hoy en IA. Pulsa una fuente para leer la noticia completa en su idioma original.
- Habr Machine Learning (RU)Leer la noticia completa en Habr Machine Learning (RU)
También ese día
Todas las noticias de IA del lunes 2 de noviembre de 2026 ->