Axiom Math publicó una versión verificada por máquina de The Stacks Project, una importante obra de referencia de código abierto sobre geometría algebraica. La formalización traduce las matemáticas del proyecto a cerca de 16 millones de líneas de código Lean, que un programa de verificación de pruebas comprueba paso a paso. Axiom afirma que investigadores y agentes de IA pueden usar los resultados como una biblioteca interconectada para construir nuevas pruebas formales.
Las fuentes ofrecen cifras ligeramente distintas sobre la extensión: TechCrunch habla de unas 7.654 páginas, mientras que Axiom describe el proyecto como una obra de alrededor de 7.500 páginas. El matemático de Columbia Johan de Jong inició la obra original en 2005, y otros matemáticos la ampliaron durante dos décadas. El trabajo de Axiom formaliza esas investigaciones ya existentes; no significa que los agentes de IA hayan descubierto por su cuenta las matemáticas que las sustentan.
¿Por qué importa que la biblioteca esté interconectada?
Una biblioteca de pruebas es útil no solo porque se hayan verificado sus teoremas individualmente, sino también porque las pruebas posteriores pueden reutilizarlos y aprovechar sus dependencias. Axiom afirma que conservó las etiquetas permanentes de The Stacks Project, de modo que las declaraciones de Lean remiten a las partes correspondientes del texto original. Su sitio web también permite consultar el texto junto al código y explorar cómo dependen unos resultados de otros.
Esto es especialmente importante en geometría algebraica, donde una prueba puede apoyarse en una larga cadena de ideas de áreas como el álgebra conmutativa, los esquemas, los haces y la cohomología. Axiom afirma que, antes de esta publicación, los investigadores disponían de mucha menos infraestructura en Lean para formalizar la geometría algebraica moderna. La biblioteca de la empresa les ofrece un punto de partida, sin obligarlos a formalizar de nuevo esos fundamentos para cada proyecto.
Una base para futuras pruebas y programas
Axiom afirma que sus agentes trabajaron en paralelo para traducir, demostrar e integrar miles de teoremas. Según TechCrunch, la empresa dio a los agentes una estructura flexible para que pudieran identificar tareas, y también entrenó sus propios modelos especializados en matemáticas. La empresa sostiene que la biblioteca terminada es la mayor biblioteca integrada y reutilizable de matemáticas formalizadas; esa es la descripción que Axiom hace de su publicación.
Este mismo tipo de verificación se emplea en ámbitos como el diseño de chips y la verificación de software. Axiom sostiene que contar con fundamentos reutilizables y verificados podría ayudar a los agentes de IA a crear sistemas más fiables a medida que escriben más código. Sin embargo, la publicación verifica la formalización de The Stacks Project, no todas las nuevas afirmaciones matemáticas ni todos los programas que pueda generar un sistema de IA.
Por qué importa
Para quienes trabajan en geometría algebraica, la biblioteca ofrece resultados verificados que pueden reutilizar, en lugar de reconstruir los mismos fundamentos en Lean. Confirma la formalización de esta obra de referencia, pero no demuestra que las futuras pruebas o el código generados por IA sean fiables sin verificación.
