«La mayor demostración de la historia, verificada por computadora»: qué prueba de verdad Axiom con Lean e IA

Respuesta corta: según Axiom, su sistema de agentes de IA (AxiomProver) escribió en 24 días una demostración completa en Lean de la clasificación de los grupos finitos simples (CFSG), uno de los teoremas más largos de la matemática. El código es público y, según su README, no tiene sorry y usa solo los tres axiomas estándar de Lean. Lo que todavía falta es que alguien fuera de Axiom reconstruya la prueba y que expertos confirmen que el enunciado en Lean dice lo mismo que el teorema. Lean garantiza que los pasos son correctos. Que el enunciado sea el correcto lo tienen que revisar personas.

El martes 27 de octubre a las 11:34 (hora de Argentina), la cuenta oficial de Axiom en X publicó: "La demostración matemática más grande de la historia humana ahora está verificada por computadora". Ese mismo día apareció el repositorio público con el código, y el blog de la empresa contó el proceso con bastante detalle.

Si programas con agentes, esta noticia te importa por una razón concreta: es el caso más grande hasta ahora de agentes produciendo trabajo que una máquina puede comprobar sin confiar en ellos. Esa idea sirve también para el código que esos agentes escriben en tu repositorio.

En esta nota separo lo comprobado de lo afirmado, explico qué revisa Lean y qué deja afuera, y cierro con pasos concretos para probar Lean y con los casos donde la verificación formal ya es útil hoy.

Qué dice Axiom, según su blog y su repositorio

El teorema dice, en simple, que todo grupo finito simple pertenece a alguna de las familias conocidas o es uno de los 26 grupos esporádicos, entre ellos el llamado Monstruo. La demostración original, según el blog de Axiom, ocupa unas 15.000 páginas repartidas en más de 500 artículos de alrededor de 100 matemáticos. Según Axiom, ninguna persona la leyó entera.

Según ese mismo blog:

• Durante 24 días, ingenieros y matemáticos de Axiom dirigieron "enjambres de decenas de agentes de IA" que produjeron aproximadamente 43,1 millones de líneas de Lean.
• El proyecto arrancó el 1 de octubre con un canal de Slack y un mapa de la prueba armado a partir de la literatura publicada, dividido en 108 hitos y unas 380 tareas. Los agentes tomaban tareas y reportaban avances por issues de GitHub y Slack.
• El trabajo se apoya en Mathlib e incorpora unas 1,2 millones de líneas del proyecto Qiuzhen-CFSG.
• Al traducir la prueba a Lean aparecieron problemas en lo publicado: la mayoría menores (erratas, errores en tablas, hipótesis omitidas) y "34 desviaciones notables" que hubo que resolver.

Según el README del repositorio, la prueba es "libre de sorry", está escrita para Lean 4 v4.35.0-rc3, se apoya en Mathlib y en el proyecto TauCeti, y usa solo los axiomas estándar Classical.choice, propext y Quot.sound, sin native_decide. El enunciado final no lo escribió Axiom: lo toma del proyecto TauCeti. La licencia es Apache 2.0.

El sitio del proyecto muestra 43,1 millones de líneas, 2,05 millones de declaraciones y la frase "cada paso lógico comprobado por el kernel de Lean".

### Ahora las salvedades, y pesan

La primera es de números. El hilo oficial en X habla de "50 millones de líneas de Lean" y de que la IA "corrigió cientos de erratas importantes". El blog dice 43,1 millones y 34 desviaciones notables. En esta nota uso las cifras del blog y del repositorio, que son más precisas.

La segunda es de tiempos. Al cierre de esta nota no encontré una reconstrucción independiente de la prueba ni una declaración del equipo de Lean (Lean FRO) o de los mantenedores de Mathlib. La propia Axiom invita a "volver a correr la comprobación y confirmar que el enunciado en Lean dice lo que dice CFSG". Esa invitación es honesta, y también muestra que el paso todavía no está hecho.

La tercera es de práctica: según el README, construir el proyecto completo con lake build les llevó cerca de 24 horas, y eso usando cambios a Lake que todavía no están integrados en la versión oficial. Reproducirlo no es algo que hagas en tu laptop una tarde.

La cuarta es de independencia. Varias de las voces más entusiastas en X trabajan en Axiom o están vinculadas a la empresa. La lista de erratas, según el blog, se publicará después, en consulta con expertos.

Estado: código público y verificable en principio; validación externa pendiente.

El giro: la IA encontró un hueco en un argumento publicado

La parte más interesante no es el tamaño. Según el blog y el artículo que acompaña el anuncio, los agentes encontraron contraejemplos a una afirmación usada en la demostración publicada en 1986 del Teorema del Grupo No Balanceado (UGT), una pieza central de la primera generación de la prueba.

Esto no tumba el teorema. El artículo aclara que la obstrucción afecta a ese argumento en particular y que el UGT tiene otras demostraciones. Para cerrar el hueco, según Axiom, AxiomProver probó un resultado nuevo apoyado en la teoría de 2-componentes maximales que Ronald Solomon desarrolló en 1976.

Otro ejemplo del blog: en los volúmenes "quasithin" de Aschbacher y Smith, un lema afirmaba que dos cantidades eran iguales. Los agentes encontraron un contraejemplo con el grupo SL₂(5), donde una vale 1 y la otra 2. Cambiar la igualdad por una desigualdad arregló el lema, pero obligó a revisar argumentos posteriores que dependían de ella.

Para quien programa, la lección es directa: un verificador estricto no solo confirma, también encuentra errores que décadas de revisión humana dejaron pasar. Y lo hace sin necesidad de confiar en quien escribió el código, sea una persona o un agente.

Hay un detalle del blog que conviene leer dos veces. Al principio, algunos hitos "manejables" escondían requisitos enormes que los agentes habían supuesto en lugar de probar. Axiom borró decenas de miles de líneas construidas sobre esos supuestos. El blog explica además que Lean puede aceptar una prueba hecha bajo una hipótesis extra no demostrada, así que la revisión tuvo que comparar cada enunciado probado con el objetivo real. Es el mismo problema que tienes cuando un agente "pasa los tests" porque cambió el test.

La cronología, con recibos

| Cuándo | Quién | Qué pasó | Resultado | |---|---|---|---| | 1976 | Ronald Solomon | Teoría de 2-componentes maximales | Base del resultado nuevo, según el artículo | | 1986 | Walter | Publica una ruta de prueba del UGT | Axiom encuentra contraejemplos a un paso, según su blog | | 2004 | Aschbacher y Smith | Volúmenes "quasithin" (1.221 páginas) | Cierra la primera generación de la prueba, según el blog | | 11-ago-2026 | Nie, Zhang, Tang, Testa, Yau | Artículo FormaTheoria en arXiv | Trabajo previo hacia formalizar CFSG | | 1-oct-2026 | Axiom | Abre el canal del proyecto | 108 hitos y unas 380 tareas, según el blog | | 10-oct-2026 | Agentes de Axiom | "Probamos que el Monstruo es simple" | Hito intermedio, según el blog | | 26-oct-2026 | Axiom | Fecha del post "Formalizing the Enormous Theorem" | Relato oficial del proceso | | 27-oct-2026, 10:19 ART | Axiom | Se crea el repositorio público en GitHub | Código bajo Apache 2.0 | | 27-oct-2026, 11:34 ART | @axiommathai | Hilo de anuncio en X | Más de 100.000 impresiones en pocas horas |

Probado, afirmado y rumor

| Afirmación | Estado | Por qué | |---|---|---| | Existe un repositorio público con la prueba en Lean | Probado | Está en GitHub, con licencia Apache 2.0 | | La prueba no usa sorry ni axiomas extra | Afirmado | Lo dice el README; el repositorio incluye una configuración de comparator que solo permite los tres axiomas estándar, pero no encontré una reconstrucción externa | | Unas 43,1 millones de líneas en 24 días | Afirmado | Según el blog y el sitio de Axiom | | "50 millones de líneas" | Afirmado e inconsistente | Aparece en el hilo de X y no coincide con el blog | | 34 desviaciones notables respecto de lo publicado | Afirmado | Según el blog; la lista de erratas aún no está publicada | | "Cientos de erratas importantes" | Afirmado e inconsistente | Según el hilo de X; el blog habla de 34 notables y muchas menores | | Contraejemplos a un paso de la prueba del UGT de 1986 | Afirmado, con detalle | Explicado en el artículo de Axiom; falta revisión de terceros | | El enunciado en Lean expresa fielmente CFSG | Pendiente | Axiom misma pide a especialistas que lo confirmen | | "Más de 2.000 errores encontrados" | Rumor | Lo dice un post en X sin fuente; no figura en el blog | | "Resuelto más allá de toda duda" | Exageración | Frase de un post en X; la validación externa todavía no ocurrió |

Qué verifica Lean y qué no

La documentación oficial de Lean tiene una página entera sobre esto: Validating a Lean Proof. Vale la pena leerla completa. Resumo lo que importa.

Lo que Lean sí comprueba. El kernel de Lean acepta una prueba solo si cada paso se deduce de las definiciones, teoremas y axiomas disponibles. Con #print axioms puedes ver de qué axiomas depende un teorema. Si aparece sorryAx, hay partes sin probar. Si aparece cualquier axioma fuera de propext, Classical.choice y Quot.sound, el teorema vale solo si ese axioma extra es cierto.

Lo que Lean no comprueba. Que el enunciado signifique lo que crees. La documentación lo separa explícitamente: una cosa es "¿el teorema tiene una prueba válida?" y otra "¿qué significa el enunciado?". El blog de Axiom dice lo mismo con otras palabras: las personas revisan el enunciado y sus definiciones, y Lean revisa las deducciones.

Una frase que conviene memorizar. La misma documentación clasifica como potencialmente maliciosas, a efectos de verificación, las "pruebas y programas generados por IA sin revisar". No es un juicio sobre la IA: es la postura correcta para cualquier código del que no conoces la intención. Para esos casos recomienda el nivel más alto de control: lean4checker para volver a pasar las pruebas por el kernel, y comparator, que compila la prueba en un entorno aislado y verifica que el teorema probado coincida con un enunciado de confianza escrito aparte.

El repositorio de Axiom trae justamente un archivo comparator.json con un módulo de desafío, un módulo de solución y la lista de axiomas permitidos. Es la estructura correcta para que un tercero valide la prueba. Que alguien la haya ejecutado de forma independiente es otra cosa, y todavía no lo vi publicado.

Qué significa para el código que escriben agentes

El patrón que muestra Axiom se traslada bastante bien al desarrollo de software:

1. Los agentes rinden donde se pueden verificar solos. En matemáticas formales, el verificador es Lean y no negocia. En tu repositorio, lo más parecido son el compilador, el sistema de tipos, los tests y los análisis estáticos. Cuanto más estricto sea ese verificador, más puedes delegar.
2. El cuello de botella se mueve a la especificación. Si el agente escribe el código y también el test, el test puede ser tan débil como el código. En Lean pasa igual: un enunciado mal escrito se puede probar perfectamente y no significar nada útil.
3. Los supuestos son el modo de falla silencioso. Los agentes de Axiom asumieron requisitos en lugar de probarlos. En software, el equivalente es un mock que siempre devuelve éxito, un TODO que se queda o un // @ts-ignore. Búscalos como Lean busca sorryAx.
4. La escala tiene costo de infraestructura. Axiom tuvo que distribuir resultados de compilación en caché entre máquinas y sacar los cálculos pesados a certificados verificables por separado. Si pones muchos agentes a trabajar en paralelo, tu CI va a ser el próximo cuello de botella.

Checklist para probar Lean y usar verificación formal hoy

1. Instala Lean. La vía recomendada en la página oficial de instalación es VS Code con la extensión oficial de Lean 4, que te guía por el resto. Si solo quieres mirar, Lean en el navegador funciona sin instalar nada.

2. Crea un proyecto y compílalo. Con Lean instalado (el gestor de versiones se llama elan):

bash lake new demo cd demo lake build

Para proyectos que usan Mathlib, sigue la guía de la comunidad.

3. Escribe un teorema y pregunta de qué depende.

```lean theorem suma_conmuta (a b : Nat) : a + b = b + a := by omega

#print axioms suma_conmuta -- En Lean 4.35.0 responde: -- 'suma_conmuta' depends on axioms: [propext, Quot.sound] ```

4. Mira qué pasa con una prueba incompleta.

```lean theorem pendiente (n : Nat) : n * 0 = 0 := by sorry

#print axioms pendiente -- Lean avisa que la declaración usa 'sorry' -- y la lista de axiomas incluye sorryAx ```

5. Ve cómo una especificación débil se prueba igual.

```lean -- "La salida está ordenada" no alcanza: -- una función que siempre devuelve [] lo cumple. def miOrden (_xs : List Nat) : List Nat := []

theorem miOrden_ordena (xs : List Nat) : (miOrden xs).Pairwise (· ≤ ·) := by simp [miOrden] ```

La prueba es correcta y la función es inútil. Falta pedir que la salida sea una permutación de la entrada. Es exactamente la revisión que Axiom pide para el enunciado de CFSG, en miniatura.

6. Añade la comprobación a tu CI. La documentación de Lean recomienda correr lean4checker en integración continua y señala que la acción lean-action de GitHub lo activa con lean4checker: true. Si aceptas pruebas que escribió un agente, define tú el enunciado en un archivo aparte y usa comparator para compararlas contra él.

7. Elige bien dónde usarla. La verificación formal compensa en piezas chicas y críticas: funciones de parseo y serialización, reglas de autorización, cálculos de dinero, algoritmos con invariantes claras y protocolos. Para una pantalla de configuración, los tests de siempre siguen siendo más baratos.

8. Aprende con material oficial. Theorem Proving in Lean 4 explica los axiomas, y Functional Programming in Lean enseña a usar Lean como lenguaje de programación. Según Lean en X, el 7 de noviembre hay un encuentro sobre verificación de software en Lean en Stanford, co-organizado por Beneficial AI Foundation y Lean FRO.

Conclusión

Axiom publicó algo que se puede comprobar, y eso ya lo separa de la mayoría de los anuncios de IA. El repositorio existe, la estructura para validarlo de forma independiente está, y el relato técnico es detallado y admite errores propios. Lo que no hay todavía es la confirmación externa: nadie fuera de Axiom reconstruyó públicamente la prueba, la lista de erratas no está publicada y los números del hilo en X no coinciden con los del blog.

Para quien desarrolla con agentes, la lección sirve con o sin esa confirmación: un agente es tan confiable como el verificador que lo controla y como la especificación contra la que lo verificas. Lean pone muy alto el primer listón. El segundo sigue siendo trabajo tuyo.

Preguntas frecuentes

¿Qué anunció Axiom el 27 de octubre de 2026? Según su blog y su cuenta oficial en X, una demostración completa en Lean de la clasificación de los grupos finitos simples, escrita en 24 días por enjambres de agentes de IA dirigidos por su equipo, con unas 43,1 millones de líneas de código.

¿Está verificada de forma independiente? Al cierre de esta nota, no encontré una reconstrucción pública hecha por terceros ni una declaración de Lean FRO o de Mathlib. Axiom invitó a la comunidad a hacerla.

¿Qué garantiza Lean exactamente? Que cada paso de la prueba se deduce de las definiciones y axiomas declarados. No garantiza que el enunciado formal diga lo que se quería decir; eso lo revisan personas.

¿La IA encontró errores en la demostración original? Según Axiom, sí: 34 desviaciones notables y contraejemplos a un paso de una prueba del Teorema del Grupo No Balanceado publicada en 1986. El teorema sigue siendo cierto, y Axiom dice haber probado un resultado nuevo para reemplazar ese paso.

¿Son 43 o 50 millones de líneas? El blog y el sitio del proyecto dicen unas 43,1 millones; el hilo en X dice 50 millones. La cifra más precisa es la del blog.

¿Puedo correr la verificación yo mismo? El código es público, pero según el README la compilación completa llevó cerca de 24 horas con cambios a Lake aún no integrados en la versión oficial. Para aprender, empieza con un proyecto chico y #print axioms.

¿Sirve la verificación formal para código de producción? Sí, en piezas acotadas y críticas donde puedes escribir una especificación clara. Para el resto, el compilador, los tipos y los tests cubren mejor la relación entre costo y beneficio.

Fuentes

• Axiom: Formalizing the Enormous Theorem (blog, 26-oct-2026)
• Sitio del proyecto CFSG de Axiom
• Repositorio AxiomMath/CFSG en GitHub
• Enunciado de CFSG en el proyecto TauCeti
• Artículo de Axiom: The Unbalanced Group Theorem (Hexagon)
• Hilo de anuncio de Axiom en X
• Axiom en X: 50 millones de líneas en 24 días
• Axiom en X: el Teorema del Grupo No Balanceado
• Axiom en X: invitación a validar la prueba
• Lean: Validating a Lean Proof
• Lean: instalación
• Lean en el navegador
• Theorem Proving in Lean 4: axiomas y computación
• Functional Programming in Lean
• Comunidad Lean y Mathlib: crear un proyecto
• FormaTheoria en arXiv (ago-2026)
• Lean en X: encuentro sobre verificación de software en Stanford