La startup de inteligencia artificial «Axiom Math» anunció el éxito de su sistema de agentes autónomos en la verificación formal (Formal Verification) de todo el contenido del «Stacks Project», considerado uno de los repositorios matemáticos abiertos más grandes compilados por matemáticos a lo largo de la historia.
Transformando el conocimiento matemático en código auditable
El proyecto Stacks, iniciado por el profesor de matemáticas de la Universidad de Columbia, Johan de Jong, en 2005, incluye unas 7,654 páginas que cubren principios de álgebra y geometría algebraica, hasta teorías avanzadas en teoría de números. Los enjambres de agentes de Axiom Math lograron traducir estos textos complejos e interconectados en aproximadamente 16 millones de líneas de código en «Lean», un lenguaje de programación especializado que permite a los programas de auditoría revisar cada prueba matemática línea por línea para asegurar su estricta integridad lógica.
La empresa, que cuenta con una valoración de mercado de 1.6 mil millones de dólares tras recaudar 200 millones de dólares en una ronda de financiación inicial liderada por «Menlo Ventures», tiene como objetivo construir una base de conocimientos confiable y verificada por software. Esto permitirá que los sistemas de inteligencia artificial del futuro se apoyen en ella para el desarrollo de software y la investigación científica, evitando la generación de conclusiones engañosas o inexactas conocidas como «basura generativa» (AI slop).
Mecanismo de trabajo de los agentes de software y desafíos de la interconexión estructural
Carina Hong, fundadora y directora ejecutiva de la empresa, de 25 años de edad, quien dejó su programa de doctorado en matemáticas en la Universidad de Stanford para fundar Axiom en marzo de 2025, explicó que el mayor desafío fue mantener la coherencia de miles de teoremas y evitar cualquier contradicción conceptual. Por su parte, Ashvin Swaminathan, miembro del equipo técnico de la empresa, señaló que los agentes de inteligencia artificial no trabajaron bajo una dirección directa para cada paso, sino que se les asignó una estructura jerárquica flexible que les permitió distribuir tareas en paralelo y aprovechar modelos personalizados entrenados en el razonamiento matemático sólido, en lugar de depender de modelos de generación de código de propósito general.
¿Qué significa este logro para el sector tecnológico?
Este desarrollo representa un paso práctico para cerrar una brecha importante en la demostración matemática computacional, especialmente en campos como la geometría algebraica. La utilidad de la verificación formal no se limita a los círculos académicos; documentar pruebas a través de código informático proporciona un entorno fundamental reutilizable. La empresa apuesta a que los desarrolladores y los creadores de software crítico —como el diseño de chips y los cálculos de sistemas críticos— necesitarán estas bases verificadas para prevenir vulnerabilidades de seguridad y errores ocultos derivados de la creciente dependencia de los agentes en la escritura de software.