AxiomMath, una startup de inteligencia artificial con sede en San Francisco y una valoración de 1.600 millones de dólares, ha anunciado un hito histórico: la verificación formal completa del Proyecto Stacks, uno de los cuerpos más extensos de matemáticas escritas por humanos. Este logro, revelado el miércoles, posiciona a la empresa como un actor clave en la búsqueda de una base matemática verificada que permita a los agentes de IA escribir software fiable y, a largo plazo, realizar descubrimientos científicos rigurosos, evitando así el fenómeno conocido como 'slop' de IA, donde la generación de contenido de baja calidad o erróneo se vuelve predominante.
El Proyecto Stacks, iniciado en 2005 por el matemático Johan de Jong de la Universidad de Columbia, es una referencia de código abierto que abarca desde la álgebra de nivel universitario hasta las ideas más avanzadas de la geometría algebraica y la teoría de números. Según Peter Woit, matemático de la Universidad de Columbia, Stacks es comparable a los famosos libros de Bourbaki, reconstruyendo las matemáticas desde sus fundamentos. AxiomMath ha traducido las aproximadamente 7.654 páginas de este manuscrito en unos 16 millones de líneas de código verificado en el lenguaje Lean, utilizando un asistente de pruebas que revisa cada línea para garantizar la coherencia lógica.
La verificación formal es una disciplina que permite confirmar que un sistema o diseño funciona exactamente como se espera, sin errores lógicos ocultos. Aunque los ingenieros la utilizan para verificar diseños de chips y los investigadores franceses han detectado errores en software de cálculo familiar, su aplicación en matemáticas es más compleja debido a la interconexión de los teoremas. En Stacks, cada resultado depende de los anteriores, formando una estructura jerárquica similar a un árbol genealógico. Carina Hong, CEO de AxiomMath, de 25 años y ex estudiante de doctorado en Stanford, admitió que el equipo tuvo dudas iniciales sobre si la 'vibe coding' (programación asistida por IA) podría preservar la belleza y la consistencia de Stacks. Para resolver esto, el equipo impuso una jerarquía controlada pero no dictatorial, permitiendo que los agentes de IA trabajaran en paralelo y se autoseleccionaran tareas, manteniendo la integridad de las conexiones matemáticas.
AxiomMath ha adoptado un enfoque distintivo: ha entrenado sus propios modelos de IA especializados en matemáticas, algo que otras startups de verificación formal no han hecho. Esto ha permitido que los agentes desarrollen un 'sentido del gusto' matemático propio, superando la necesidad de depender exclusivamente de expertos humanos para guiar cada paso. El resultado es una librería reutilizable que cubre un vacío significativo en la matemática formalizada, particularmente en geometría algebraica, donde antes los investigadores carecían de una base sólida para verificar nuevos resultados con Lean.
El impacto de este proyecto trasciende la academia. Para los desarrolladores, que luchan por garantizar la ausencia de errores y vulnerabilidades de seguridad en su código, AxiomMath ofrece una infraestructura de confianza. Los teoremas verificados se convierten en bloques de construcción para futuras pruebas, permitiendo que la comunidad científica y tecnológica construya sobre matemáticas ya comprobadas en lugar de partir de cero. Terence Tao, ganador de la Medalla Fields, ha destacado la importancia de esta formalización, señalando que cuanto más pruebas formales se tengan, más formales se pueden crear, acelerando el avance del conocimiento.
La empresa ha recaudado 200 millones de dólares en su ronda Serie A, liderada por Menlo Ventures, y ha lanzado esta verificación como un desafío abierto a otras empresas de codificación. AxiomMath argumenta que la matemática es el dominio donde se construyen estas habilidades transferibles; los agentes de IA pueden leer y entender el código formalizado de Axiom para construir nueva infraestructura. Al proporcionar una librería reutilizable y robusta, AxiomMath busca evitar que los agentes de IA caigan en decisiones de ingeniería deficientes que limiten su capacidad de crecimiento, estableciendo un nuevo estándar para la fiabilidad en la era de la inteligencia artificial.