Parece que la inteligencia artificial está resolviendo casi cada semana un nuevo problema matemático. El mes pasado, solo OpenAI publicó 719 manuscritos que afirman haber resuelto algunos de los problemas más difíciles del campo. Incluso la verificación por computadora puede cometer errores. Tras años de contenido basura generado por IA, uno no puede evitar preguntarse si las matemáticas serán el próximo campo afectado.
AxiomMath puede evitar este destino no ralentizando el ritmo, sino construyendo una base más sólida. Esta startup valorada en 1.600 millones de dólares espera crear una capa de base verificada sobre la cual los agentes de IA puedan confiar para escribir software y, finalmente, realizar investigación científica.
El miércoles, la empresa anunció que ha verificado oficialmente el proyecto Stacks, uno de los mayores logros matemáticos escritos por humanos. Los matemáticos suelen evaluar muy altamente Stacks. El matemático de la Universidad de Columbia Peter Woit lo describió como “casi nada más puede compararse con ello” y comparó el proyecto con la famosa serie Bourbaki, la colección de obras que reconstruyeron las matemáticas desde sus fundamentos durante el siglo XX.
El colega colombiano de Woit, Johan de Jong, lanzó el Proyecto Stacks en 2005 como una referencia de código abierto. Desde entonces, los matemáticos han contribuido con contenido que abarca desde álgebra a nivel universitario hasta las ideas más avanzadas en álgebra, geometría y teoría de números.
El grupo de agentes de IA de la empresa tradujo esta base de datos de aproximadamente 7,654 páginas en alrededor de 16 millones de líneas de código verificables por computadora.
El propósito de las matemáticas formalizadas es garantizar que su estructura subyacente sea confiable. Los matemáticos reescriben las demostraciones como código utilizando un lenguaje de programación llamado Lean, y luego un programa llamado asistente de prueba verifica línea por línea ese código. Si la demostración pasa la verificación, los matemáticos pueden confiar en que es lógicamente válida.
Los ingenieros también utilizan el mismo enfoque, es decir, la verificación formal, para confirmar si el diseño de los chips es viable; los investigadores franceses lo utilizaron para descubrir una vulnerabilidad en el software de cálculo de subsidios familiares.
Para un repositorio como el Proyecto Stacks, revisar teoremas uno por uno es solo parte del trabajo. Los teoremas y definiciones en Stacks están interconectados, y cada uno se construye sobre los anteriores. Como un árbol genealógico, muchos resultados en Stacks pueden rastrearse hasta resultados anteriores.
Esta interconexión hizo que Axiom no estuviera segura al principio de si el proyecto era viable. El equipo debía mantener intactas todas las conexiones dentro de aproximadamente 16 millones de líneas de código Lean.
El CEO de Axiom, Carina Hong, le dijo a TechCrunch: “En la realidad, el volumen y la precisión generalmente no son compatibles. [Stacks] es un conjunto de resultados matemáticos que constituyen la base matemática. Deseas que los [teoremas] sean coherentes entre sí, no como paradojas. También deseas que estas definiciones no entren en conflicto entre sí.”
Este CEO de 25 años dejó el programa de doctorado en matemáticas de Stanford y fundó esta empresa en marzo de 2025. En marzo de este año, Axiom completó una ronda de financiación Serie A de 200 millones de dólares liderada por Menlo Ventures.
Hong dijo: "No estábamos seguros de si vibe coding podría conservar la estética de Stacks."
Para completar este proyecto, el equipo estableció una estructura flexible para los agentes y los ejecutó en paralelo. Ashvin Swaminathan, miembro del equipo técnico de Axiom, dijo: “Para Stacks, establecimos una jerarquía... pero no una en la que se especifique exactamente qué debe hacer cada agente. Los agentes buscan sus propias tareas e identifican qué se puede procesar en paralelo.”
Axiom también entrenó sus propios modelos para que sean expertos en matemáticas. Hong dice que esta práctica no la han adoptado la mayoría de las otras startups de validación. Inicialmente, el equipo dependía de un experto interno en Lean para enseñar a los agentes a formar criterios de juicio similares a los humanos. Con el tiempo, dice Hong, estos agentes han aprendido por sí mismos este juicio.
Este logro llena uno de los mayores vacíos en las matemáticas formalizadas. "Cuando miras el contenido matemático que ya ha sido formalizado, encuentras un enorme agujero negro. Y ese agujero negro abarca la geometría algebraica", dice Swaminathan.
Swaminathan dijo que, hasta ahora, los investigadores que querían usar Lean para verificar nuevos trabajos en geometría algebraica tenían muy poca base disponible. "Ahora la tienen."
Axiom cree que cada resultado verificado se convierte en un bloque de construcción, sobre el cual las demostraciones futuras pueden basarse en matemáticas ya verificadas, sin necesidad de comenzar desde cero. El matemático de UCLA y ganador de la Medalla Fields, Terence Tao, resumió esto de manera más concisa: "Cuanto más pruebas formalizadas tengas, más pruebas formalizadas podrás hacer."
El público objetivo de Axiom no solo son los matemáticos. Los desarrolladores han estado trabajando durante mucho tiempo para asegurar que su código esté libre de vulnerabilidades y riesgos de seguridad. Con la creciente cantidad de software escrito por agentes de IA, este problema solo se volverá más grande.
Axiom apuesta: el software del futuro debe construirse sobre bases comprobadas, al igual que Stacks hoy en día.
Swaminathan dijo: "Creemos que las matemáticas son el ámbito en el que comienzas a construir estas cosas, y es una habilidad transferible. Los agentes pueden leer nuestro código, comprenderlo y construir nueva infraestructura sobre él. Lo que hemos formalizado con Lean es ahora la base subyacente sobre la que los agentes pueden construir."
La forma en que Axiom construye agentes para Stacks —trabajar en paralelo y elegir sus propias tareas— es precisamente la forma en que Hong espera que muchos trabajos de IA se realicen en el futuro. Ella cree que los agentes de IA necesitan una base de conocimiento bien estructurada y reutilizable para evitar generar contenido de baja calidad.
Hong dijo: "Esperas que el [agente] tenga una biblioteca reutilizable sobre la cual pueda seguir construyendo y empujando constantemente los límites. Si desde el principio introduces basura con malas decisiones de ingeniería, será muy difícil que amplíe ese límite."
Hong tiene mucha confianza en este método e incluso lanzó públicamente un desafío. Dijo: "Desafío públicamente a todas las empresas de programación a realizar este tipo de trabajo formalizado a esta escala."