Axiom publica una formalización en Lean de todo el Stacks Project, unos 16 millones de líneas creadas por enjambres de agentes de IA
La referencia de geometría algebraica de unas 7.500 páginas es ahora una única biblioteca verificada por máquina; matemáticos externos aún no han revisado la fidelidad de los enunciados.
Por qué importa
La geometría algebraica moderna apenas tenía infraestructura en Lean, porque una sola demostración puede depender de largas cadenas de resultados de álgebra conmutativa, esquemas, haces y cohomología. Axiom afirma que su biblioteca conserva las etiquetas permanentes del Stacks Project, de modo que personas y agentes de IA pueden importar sus definiciones y teoremas en nuevas demostraciones. Llega tras la formalización en Lean de la Clasificación de los Grupos Simples Finitos que Axiom publicó el 27 de octubre de 2026. Habrá que ver si los matemáticos que contrasten los enunciados con el texto original los consideran fieles y si la biblioteca se adopta junto a Mathlib.
Datos clave
- Stacks Project: unas 7.500 páginas
- Unos 16 millones de líneas de código Lean
- Hecho con enjambres coordinados de agentes de IA
- Iniciado por Johan de Jong, de la Universidad de Columbia, en 2005
- Consultable en stacks.axiommath.ai
- Sigue a la formalización CFSG de Axiom del 27 de octubre de 2026