El Proyecto Stacks sirve como una enciclopedia fundamental para la geometría algebraica moderna, un campo que estudia la relación entre las ecuaciones algebraicas y las formas geométricas. Iniciado en 2005 por Johan de Jong, el proyecto organizó décadas de conocimiento matemático disperso —que abarca álgebra conmutativa, haces y cohomología— en una referencia unificada y autónoma. Debido a que proporciona los bloques de construcción esenciales para estructuras complejas como los stacks algebraicos, a menudo se le compara con un 'kernel de Linux' para las matemáticas: una biblioteca masiva de código abierto donde cada teorema está explícitamente vinculado a sus supuestos y dependencias subyacentes.
Esta imagen ilustra la escala masiva y la estructura jerárquica del Proyecto Stacks, que Axiom está formalizando en una biblioteca verificada por máquina.
Estas figuras representan el linaje histórico de los conceptos matemáticos organizados por el Proyecto Stacks.
A medida que la inteligencia artificial comienza a generar argumentos matemáticos a una velocidad que supera las capacidades de inspección humana, la verificación formal se convierte en una salvaguarda crítica. El lanzamiento de Axiom aborda un cuello de botella significativo en la geometría algebraica: si bien muchas pruebas modernas se están formalizando ahora, a menudo dependen de una larga cadena de teoremas previos que carecían de una infraestructura verificada por máquina. Para cerrar esta brecha, Axiom tradujo el Proyecto Stacks a Lean, un lenguaje de prueba formal. Este esfuerzo implicó gestionar 16 millones de líneas de código, una tarea que requirió más que simples scripts aislados. Para mantener una biblioteca coherente donde las definiciones permanezcan compatibles a través de miles de lemas entrelazados, Axiom desplegó un sistema jerárquico de agentes de IA coordinados. Estos agentes trabajaron en paralelo para traducir enunciados, buscar abstracciones existentes en la biblioteca Mathlib y resolver requisitos previos, asegurando que cada definición permaneciera alineada en toda la base de código.
El proceso de formalización también sirvió como una herramienta para el refinamiento matemático. Durante el proyecto, el sistema identificó docenas de enunciados en el Proyecto Stacks original que requerían correcciones locales, como hipótesis faltantes o casos límite en características matemáticas específicas. En lugar de ver estos fallos como errores, los agentes diagnosticaron las obstrucciones subyacentes y construyeron contraejemplos explícitos para demostrar dónde los enunciados originales estaban incompletos. Estas resoluciones permitieron al equipo reparar las matemáticas para que los capítulos posteriores pudieran seguir funcionando. Si bien esta formalización en Lean es un proyecto de código abierto independiente mantenido por Axiom, preserva la estructura de etiquetas permanentes del Proyecto Stacks original, permitiendo a los investigadores ver el texto informal junto con el código verificado por máquina en stacks.axiommath.ai. Este hito proporciona un punto de partida verificado tanto para matemáticos humanos como para agentes de IA para explorar nuevas fronteras en la geometría algebraica y sus campos vecinos.