Axiom formaliza en Lean el Stacks Project completo: 16 millones de líneas de matemáticas verificadas por máquina
The Stacks Project, Formalized in Lean
Axiom ha publicado la formalización en Lean del Stacks Project, la referencia abierta de 7.500 páginas sobre geometría algebraica moderna. Con unos 16 millones de líneas de código, es la mayor biblioteca integrada de matemáticas formalizadas jamás construida. El proyecto conserva las etiquetas permanentes del texto original y permite a investigadores y agentes de IA importar definiciones y teoremas directamente. Para lograrlo, Axiom desplegó enjambres coordinados de agentes de IA que tradujeron y probaron miles de teoremas en paralelo, manteniendo la coherencia de las definiciones en todo el código.
En lugar de tratar los intentos de prueba fallidos como meros obstáculos, nuestros agentes diagnosticaron las obstrucciones matemáticas subyacentes y construyeron contraejemplos explícitos para demostrar dónde fallaban los enunciados originales.