Axiom Math logra la verificación formal del enorme Proyecto Stacks para asegurar las matemáticas impulsadas por IA

Image: TechCrunch · Source

Axiom Math ha verificado formalmente el extenso Proyecto Stacks utilizando agentes de IA, creando una base sólida para pruebas matemáticas confiables y allanando el camino para matemáticas y desarrollo de software asistidos por IA de manera fiable.

La rápida llegada de pruebas matemáticas generadas por inteligencia artificial ha generado inquietudes sobre la fiabilidad y precisión de tales trabajos. En los últimos meses, modelos de IA han presentado cientos de manuscritos que afirman resolver problemas matemáticos difíciles, aunque incluso las revisiones computacionales tradicionales a veces han fallado en detectar errores. Con el objetivo de afrontar este desafío, Axiom Math, una startup valorada en 1.600 millones de dólares, se centra en construir fundamentos matemáticos rigurosamente verificados mediante verificación formal, garantizando que los sistemas de IA puedan generar y utilizar matemáticas correctas con fiabilidad.

El 5 de noviembre de 2026, Axiom Math anunció un logro histórico: la verificación formal del Proyecto Stacks, uno de los compendios matemáticos más grandes y respetados. Creado en 2005 por el matemático de Columbia Johan de Jong, el Proyecto Stacks ha crecido hasta convertirse en un trabajo colaborativo y de código abierto que abarca una amplia gama de temas desde álgebra hasta geometría y teoría de números, con aproximadamente 7.654 páginas.

Los agentes de IA de Axiom tradujeron todo el Proyecto Stacks en cerca de 16 millones de líneas de código escritas en Lean, un lenguaje formal de pruebas. Esta traducción permitió que un software asistente de pruebas verificara rigurosamente cada demostración, confirmando la solidez lógica a lo largo de este cuerpo de trabajo extenso y profundamente interconectado. Asegurar la integridad de estos enlaces fue un desafío significativo, que la directora ejecutiva Carina Hong comparó con reconciliar estructuras delicadas dentro de un todo masivo sin contradicciones.

Fundada en marzo de 2025 por Hong, ex candidata a doctorado en matemáticas en Stanford, Axiom recaudó 200 millones de dólares en una ronda Serie A liderada por Menlo Ventures a principios de este año. El enfoque de la empresa implica otorgar a sus agentes de IA un marco flexible para colaborar, permitiendo trabajar en paralelo en diferentes tareas mientras se mantiene la estructura jerárquica general necesaria para preservar las dependencias dentro del Proyecto Stacks.

A diferencia de muchas iniciativas de verificación, Axiom invirtió en entrenar sus propios modelos de IA específicamente para dominar las sutilezas de las matemáticas y la formalización, enseñando efectivamente a los agentes a desarrollar un sentido del "gusto" matemático. Este avance llena una brecha importante en las matemáticas formalizadas, particularmente en geometría algebraica, proporcionando una base amplia y confiable para futuras pruebas formales utilizando Lean.

Más allá de las matemáticas puras, Axiom visualiza sus fundamentos verificados como críticos para el desarrollo de software, especialmente a medida que la IA genera cada vez más código. Anclando las salidas de IA en matemáticas rigurosamente verificadas, la empresa apunta a reducir errores y vulnerabilidades de seguridad prevalentes en el código escrito por IA.

Matemáticos como el Medallista Fields Terence Tao han reconocido la importancia de dicha formalización, señalando que las pruebas verificadas permiten la creación de más pruebas verificadas. Para Axiom, el Proyecto Stacks verificado es un sustrato reutilizable sobre el cual los agentes de IA pueden construir nueva infraestructura matemática y científica.

La directora ejecutiva Hong enfatiza que el futuro de la IA en investigación e ingeniería depende de cuerpos de conocimiento accesibles, reutilizables y cuidadosamente construidos para evitar la proliferación de errores o “imprecisiones”. Ella desafía a otras empresas centradas en la codificación a intentar la verificación formal a una escala similar y anticipa que agentes colaborativos de IA trabajando de manera asincrónica y estratégica se convertirán en la norma en avances científicos y de software.

Al cerrar la brecha entre el rigor matemático humano y el poder computacional de la IA, el trabajo de Axiom Math en el Proyecto Stacks representa un paso importante hacia matemáticas y creación de software asistidos por IA confiables, con potencial para transformar cómo se formalizan y amplían dominios complejos de conocimiento en los próximos años.