La startup de inteligencia artificial «Axiom Math» anunció el éxito de su sistema de agentes autónomos en la verificación formal y programática (Formal Verification) de todo el contenido del «Stacks Project», considerado uno de los referentes matemáticos abiertos más grandes compilados por matemáticos a lo largo de la historia.
Transformación del 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 a unos 16 millones de líneas de código en el lenguaje «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 programáticamente para que los sistemas de inteligencia artificial dependan de ella en el futuro 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, 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 teorías 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 las tareas en paralelo y aprovechar modelos personalizados entrenados en el razonamiento matemático sólido en lugar de depender de modelos generales de generación de código.
¿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. El beneficio de la verificación formal no se limita a los círculos académicos; documentar pruebas a través de códigos informáticos proporciona un entorno fundacional reutilizable. La empresa apuesta a que los desarrolladores y los creadores de software sensible—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.