¿Qué ocurre cuando una inteligencia artificial escribe miles de páginas de matemáticas que nadie puede revisar una por una? El riesgo no es solo recibir una respuesta equivocada: también puede crecer una montaña de resultados que parecen sólidos, pero esconden una grieta en su base.
Axiom Math, una startup valorada en 1.600 millones de dólares, quiere instalar un filtro antes de que esa montaña se vuelva inmanejable. La compañía anunció que verificó formalmente el Stacks Project, una de las bibliotecas matemáticas más extensas creadas por humanos.
El hallazgo llega después de que OpenAI publicara 719 manuscritos que afirmaban resolver problemas difíciles de las matemáticas. El volumen muestra una oportunidad, pero también expone un mecanismo delicado: incluso las herramientas informáticas diseñadas para comprobar resultados pueden fallar.
El Stacks Project fue iniciado en 2005 por Johan de Jong como una referencia abierta. Con aportes de matemáticos de distintas áreas, creció desde el álgebra universitaria hasta la geometría algebraica y la teoría de números.
También te puede interesar:Con 24 Años y Fichando Talento de Meta, Carina Hong Levanta una Empresa de Matemáticas con IA que Sorprende al SectorPeter Woit, matemático de la Universidad de Columbia, señaló que no hay nada realmente comparable a este trabajo. Incluso lo equiparó con los libros de Bourbaki, la ambiciosa colección que buscó reconstruir las matemáticas desde sus fundamentos durante el siglo XX.
Una casa con planos revisados pieza por pieza
La formalización matemática puede entenderse como la construcción de una casa. Una demostración tradicional es el plano escrito por un arquitecto: puede ser brillante, pero alguien debe interpretar cada trazo. La versión formalizada convierte ese plano en instrucciones exactas que una máquina puede revisar.
Lean, un lenguaje que expresa demostraciones como código, funciona como el inspector que revisa cada cable, caño y pared antes de permitir que la casa siga creciendo. Si una línea no encaja con las anteriores, el sistema detiene la obra.
La flota de agentes de IA de Axiom tradujo unas 7.654 páginas del Stacks Project a cerca de 16 millones de líneas de código verificable. No bastaba con aprobar teoremas aislados: cada definición debía conservar sus conexiones con los resultados que la sostienen.
Ese fue el verdadero interruptor del proyecto. Una biblioteca matemática se parece más a una red eléctrica que a una pila de hojas: si un cable central está mal conectado, el problema puede llegar a habitaciones muy lejanas.
Carina Hong, directora ejecutiva de Axiom y fundadora de la empresa en marzo de 2025, sostiene que los teoremas deben ser coherentes entre sí y que sus definiciones no pueden entrar en conflicto. La compañía entrenó modelos propios especializados en matemáticas y permitió que los agentes encontraran tareas paralelas dentro de una estructura general.
Terence Tao resumió esta dinámica con una idea simple: cuantas más pruebas formalizadas existen, más pruebas formalizadas pueden crearse.
La pieza clave para el software escrito por IA
La nueva base cubre una carencia importante: la geometría algebraica, un campo con pocos bloques previos disponibles para quienes querían trabajar con Lean. Ahora, un investigador puede tomar resultados ya comprobados y apoyarse sobre ellos, en lugar de empezar desde cero.
Además, el método tiene una aplicación práctica fuera de las matemáticas. La verificación formal ya se usa para confirmar que diseños de chips funcionan y para detectar errores en programas que calculan prestaciones familiares.
El desafío crece porque los agentes de IA escriben una parte cada vez mayor del código cotidiano. Si ese software controla pagos, datos médicos o sistemas públicos, una falla no queda encerrada en una pantalla: puede afectar decisiones reales.
Axiom apuesta a que el software del futuro necesitará una base verificada, como una vivienda necesita cimientos firmes antes de sumar nuevos pisos. La promesa no elimina todos los errores, pero ofrece algo central: que la velocidad de la IA no avance más rápido que los controles que la mantienen en pie.
Directora de operaciones en GptZone. IT, especializada en inteligencia artificial. Me apasiona el desarrollo de soluciones tecnológicas y disfruto compartiendo mi conocimiento a través de contenido educativo. Desde GptZone, mi enfoque está en ayudar a empresas y profesionales a integrar la IA en sus procesos de forma accesible y práctica, siempre buscando simplificar lo complejo para que cualquiera pueda aprovechar el potencial de la tecnología.
