Puntos clave
- AxiomProver es el clúster de demostradores con el que Axiom dice haber formalizado por completo, en Lean, la clasificación de los grupos simples finitos.
- La formalización ronda los 50 millones de líneas y se completó en 24 días; el teorema humano ocupa unas 15.000 páginas y lo construyeron más de 100 matemáticos a lo largo de generaciones.
- No hay build, descarga ni página oficial publicados: de momento solo existe el anuncio y un vídeo breve de vista previa.
Datos rápidos
| Quién lo anuncia | Axiom, el 27 de octubre de 2026 |
|---|---|
| Sistema de prueba | Lean, mediante el clúster AxiomProver |
| Escala anunciada | Unos 50 millones de líneas en 24 días |
| Acceso | Sin build, descarga ni página oficial |
| Categoría | IA y modelos |
| Creador | Axiom |
| Popularidad | 🔥 3,6M Popularidad |
| Publicado | |
| Última actualización |
Qué formalizó Axiom
La mayor demostración matemática de la historia humana ya está verificada por ordenador.
La clasificación de los grupos simples finitos, o CFSG, enumera las piezas básicas con las que se construye la simetría finita. Axiom la presenta como la tabla periódica de la simetría: un teorema de unas 15.000 páginas elaborado por más de 100 matemáticos a lo largo de varias generaciones.
La novedad no es el teorema en sí, sino su paso a una prueba que una máquina puede comprobar línea a línea. Axiom afirma que AxiomProver produjo una autoformalización completa en Lean y la sitúa como la mayor prueba matemática verificada por ordenador hasta ahora.
Escala, plazo y lo que se sabe del sistema
El único dato de arquitectura que acompaña al anuncio es que el trabajo lo hizo un clúster de demostradores de inteligencia artificial llamado AxiomProver, escribiendo la prueba en Lean. No se han publicado pesos, tamaño del clúster, método de búsqueda ni desglose de cuánto revisó una persona.
- Unos 50 millones de líneas
Esa es la cifra de código Lean que Axiom asocia a la formalización completa.
- 24 días
Es el plazo que el equipo atribuye a la generación de esa formalización con el clúster.
- Unas 15.000 páginas
Así describe Axiom la prueba humana de partida, no el tamaño del archivo Lean.
| Pieza | Dato anunciado |
|---|---|
| Prueba humana | Unas 15.000 páginas, más de 100 matemáticos |
| Formalización | Lean, clúster AxiomProver |
| Código | Unos 50 millones de líneas |
| Duración | 24 días |
Para qué serviría y qué queda abierto
Si la formalización se sostiene, el uso inmediato es de archivo y de comprobación: una biblioteca Lean en la que otros desarrollos sobre grupos finitos puedan apoyarse sin rehacer a mano miles de páginas. También sirve como prueba de estrés para un demostrador automático en un teorema que, por tamaño, casi ningún proyecto de formalización había intentado de una vez.
Compararlo con otros modelos queda limitado a lo que Axiom ha dicho. Frente a la prueba en papel, el cambio es de medio: de un texto leído por especialistas a un desarrollo que el núcleo de Lean puede verificar. No hay cifras públicas frente a otros demostradores, ni precios, ni cupos, ni API, ni pesos abiertos. La afirmación de ser la mayor prueba verificada por ordenador es la de la propia compañía.
Tampoco hay forma de probarlo. No existe build público, descarga ni página oficial; el anuncio se ha mostrado en un vídeo breve de vista previa. Queda por ver el repositorio, la revisión independiente y si cada parte de las 15.000 páginas quedó realmente cubierta.
Preguntas frecuentes
¿Puedo ejecutar AxiomProver o descargar la formalización?
No por ahora. Axiom solo ha mostrado el resultado en un anuncio y un vídeo corto de vista previa; no hay build, descarga ni página oficial.
¿AxiomProver demostró un teorema nuevo?
No según el anuncio. Formalizó en Lean la clasificación de los grupos simples finitos, un teorema ya establecido, para que un ordenador pueda verificar esa prueba.
