IA en un minutoNoticiasAgentes
Axiom Math formaliza en Lean el Stacks Project, una base matemática para agentes de IA
Redacción de IA en un minuto · Editor: Jon Elgezabal
En 30 segundos
Axiom Math ha traducido a Lean el Stacks Project completo con agentes de IA que trabajaban en paralelo, y el resultado ronda los 16 millones de líneas. Los agentes dieron con decenas de enunciados que pedían retoques y fabricaron contraejemplos para demostrarlo. Axiom guarda esos arreglos aparte, ya que Johan de Jong no quiere por ahora aportaciones de IA en el repositorio original.
Axiom Math, una startup que desarrolla IA para matemáticas, publicó el 4 de noviembre una formalización en Lean del Stacks Project completo, la referencia abierta de geometría algebraica de aproximadamente 7.500 páginas. Lean es un lenguaje en el que un ordenador comprueba cada demostración, y el resultado ocupa unos 16 millones de líneas de código. La empresa sostiene que es la mayor biblioteca de matemáticas formalizadas, conectada y reutilizable, que se ha construido.
El Stacks Project lo puso en marcha en 2005 Johan de Jong, matemático de la Universidad de Columbia, y desde entonces lo han ampliado cientos de colaboradores. Cada resultado lleva una etiqueta fija de cuatro caracteres, y la versión de Axiom la conserva: en stacks.axiommath.ai se pueden leer el texto original y el código Lean uno al lado del otro, junto con el grafo de dependencias. Según Axiom, la geometría algebraica moderna apenas tenía infraestructura en Lean, porque una sola demostración actual puede apoyarse en una larga cadena de teoremas previos.
El trabajo lo hizo un sistema jerárquico de agentes de IA diseñado por los matemáticos e ingenieros de la empresa. Los agentes avanzaron en paralelo por el grafo de dependencias: traducían enunciados, buscaban en Mathlib (la biblioteca de matemáticas de la comunidad de Lean) lo que ya existía, construían demostraciones y resolvían requisitos previos. Para comprobar que cada enunciado formal dice lo mismo que el original, Axiom combinó auditorías entre varios agentes, cotejos automáticos con el texto y revisiones dirigidas de las definiciones de base.
En el proceso aparecieron decenas de enunciados del Stacks Project que necesitaban un ajuste: hipótesis que faltaban, casos límite en característica positiva y afirmaciones que no se cumplen con toda la generalidad con la que están escritas. Los agentes construyeron contraejemplos para esos casos y, cuando un lema falso dejaba un hueco en la prueba de un teorema mayor, buscaron otra vía para demostrarlo con sus hipótesis originales.
El 21 de octubre, De Jong pidió que, por ahora, no se envíen comentarios ni cambios generados por IA directamente al repositorio del Stacks Project. Axiom mantiene la formalización como un proyecto de código abierto independiente y guarda en su propio repositorio los contraejemplos y las correcciones. Es su segunda gran formalización en pocos días: el 27 de octubre publicó la de la clasificación de los grupos simples finitos.
Según TechCrunch, Axiom, fundada en marzo de 2025 por su consejera delegada, Carina Hong, es una startup de 1.600 millones de dólares y en marzo cerró una ronda de serie A de 200 millones encabezada por Menlo Ventures. El mismo medio cifra el Stacks Project en aproximadamente 7.654 páginas; Axiom habla de unas 7.500. La empresa quiere que esta base verificada sirva de punto de partida a los agentes de IA, y en TechCrunch Hong y el equipo de Axiom la plantean también como cimiento para el software que escriban esos agentes.
Por qué importa · análisis y opinión
La formalización matemática llevaba años avanzando a mano, teorema a teorema, y la geometría algebraica era uno de sus grandes huecos. Que unos agentes de IA hayan cubierto una obra de referencia entera cambia la escala de lo posible, pero lo más útil puede ser lo que destaparon: errores en un texto revisado durante años por especialistas. La prueba de verdad llegará cuando los matemáticos empiecen a apoyarse en esta biblioteca para su propio trabajo y comprueben si es cómoda de usar, no solo correcta. También está por ver cómo convive con Mathlib y con la comunidad del Stacks Project, que ha pedido distancia a las aportaciones automáticas. Para el resto, el mensaje es otro: la IA que produce resultados necesita algo que los compruebe.
Fuente oficial: Axiom Math · Redactada con ayuda de IA: cómo hacemos las noticias
