Axiom Math verificó 16 millones de líneas de código Lean con agentes y cerró una brecha en la matemática formal

Cuando la IA «resuelve» cada semana un nuevo problema matemático, surge una pregunta razonable: ¿quién comprueba todo eso? Solo el mes pasado, OpenAI publicó 719 manuscritos con supuestas soluciones a problemas difíciles. Leerlos todos a mano es imposible, y los errores se cuelan incluso con revisiones automáticas. Axiom Math, una startup valorada en 1.600 millones de dólares, propone otro camino: no frenar, sino apoyarse en una base verificada.

Qué hicieron exactamente

El miércoles la compañía anunció que había verificado formalmente el Stacks Project, una de las mayores colecciones de matemática humana de la historia. Lo inició en 2005 Johan de Jong, de la Universidad de Columbia, como referencia abierta. Hoy tiene unas 7654 páginas: desde álgebra universitaria hasta ideas de vanguardia en geometría algebraica y teoría de números.

Los agentes de Axiom reescribieron todo ello en unos 16 millones de líneas de código en el lenguaje Lean. Después, un programa llamado proof assistant revisó el código línea por línea. Si la comprobación se supera, la demostración es lógicamente correcta y no hace falta creer al autor bajo palabra.

Por qué es más difícil de lo que parece

Verificar cada teorema por separado es solo la mitad del trabajo. Los resultados del Stacks Project están conectados como un árbol genealógico: cada uno se apoya en los anteriores. Si una definición «se desliza» en algún punto, se derrumba todo lo que está encima. Por eso el equipo tuvo que conservar todas las conexiones a lo largo de 16 millones de líneas. La propia CEO, Carina Hong, admite que al principio no estaba segura del éxito: lo grande y lo frágil combinan mal.

La arquitectura fue así: una jerarquía blanda arriba, pero sin reparto rígido de tareas. Los agentes encontraban por sí mismos en qué trabajar y lo hacían en paralelo. Axiom también entrenó modelos propios para matemáticas, algo que, según Hong, la mayoría de los competidores en verificación no hace. Primero, un experto interno en Lean inculcó a los agentes «gusto», es decir, la comprensión de cómo debe verse un buen código. Con el tiempo, dice Hong, aprendieron a arreglárselas solos.

Por qué importa a los desarrolladores

El sentido práctico no está en la geometría algebraica en sí. La verificación formal se usa desde hace tiempo donde el error sale caro: la comprobación de chips, y unos investigadores franceses la emplearon para encontrar fallos en el software que calcula las prestaciones familiares. El problema es que los agentes escriben cada vez más código, sin que aumenten las garantías de ausencia de errores y brechas de seguridad.

La apuesta de Axiom: las matemáticas son un campo de pruebas donde se perfecciona esta habilidad para luego trasladarla al software. Los agentes pueden leer una biblioteca Lean ya hecha y construir sobre ella sin empezar de cero. Terence Tao formula el principio general así: cuantas más demostraciones formalizadas haya, más cosas nuevas se pueden hacer.

Limitaciones

Por ahora es una afirmación de la propia compañía, y el material no incluye una evaluación independiente del resultado. Trasladar la habilidad de las matemáticas al código industrial es una hipótesis, no un hecho probado. El software real depende del entorno, de las dependencias y de requisitos informales que no se formalizan tan limpiamente como los teoremas. El reto de Hong a todas las empresas que escriben código para formalizar a esta escala suena contundente, pero por ahora es más bien marketing.

Qué hacer en la práctica

Si construyes sistemas de agentes para código, echa un vistazo a Lean y a la idea de artefactos verificables: que el agente entregue no solo código, sino también algo que se compruebe automáticamente. Para los equipos de producto la conclusión es más simple: «lo escribió la IA» y «lo escribió la IA y está demostrado» pronto serán dos categorías de calidad distintas. Quienes trabajan en áreas críticas, como finanzas, medicina y seguridad, deberían tener este cambio en el radar desde ya.