Qué pasó
- Axiom Math, una empresa emergente valorada en US$ 1.600 millones, anunció el miércoles 4 de noviembre de 2026 que verificó formalmente el Stacks Project. TechCrunch publicó el caso el 5 de noviembre.
- El Stacks Project es una referencia abierta que el matemático Johan de Jong, de Columbia, inició en 2005. Reúne resultados de álgebra, geometría y teoría de números, desde nivel universitario hasta los temas avanzados del área.
- La flota de agentes de IA de Axiom tradujo sus cerca de 7.654 páginas a unos 16 millones de líneas de código en Lean, un lenguaje en el que un programa llamado asistente de pruebas revisa cada demostración línea por línea.
- Los agentes corrieron en paralelo con una estructura laxa. Según Ashvin Swaminathan, de Axiom, había jerarquía, pero los agentes buscaban solos las tareas que podían abordar a la vez.
Por qué importa
- Si una demostración pasa el asistente de pruebas, se puede confiar en que es lógicamente sólida. Es otro modo de revisar matemática, distinto de la lectura por pares.
- El resultado apunta a un hueco conocido. “Hay un enorme agujero negro” en lo formalizado, y cubre la geometría algebraica, dijo Swaminathan a TechCrunch.
- La empresa ve un uso más allá de la matemática: una base verificada sobre la que agentes puedan escribir software con menos errores y fallas de seguridad.
El dato
16 millones de líneas. Es el tamaño aproximado del código en Lean. La dificultad no estaba solo en cada teorema, sino en mantener intactas las conexiones entre definiciones y resultados que se apoyan unos en otros.
Contexto
Axiom fue fundada en marzo de 2025 por Carina Hong, de 25 años, quien dejó un doctorado en matemáticas en Stanford. En marzo de este año levantó una serie A de US$ 200 millones liderada por Menlo Ventures. Hong dijo a TechCrunch que no estaban seguros de que programar con agentes preservara la estructura del Stacks, y que las definiciones no debían contradecirse entre sí.
La empresa entrenó además sus propios modelos para matemática. Al comienzo, un experto interno en Lean les enseñó criterio; con el tiempo, según Hong, lo fueron adquiriendo solos. Es una afirmación de la compañía que no pudo contrastarse con una revisión externa en la nota de TechCrunch.
En Mamífero hemos cubierto la verificación y el trabajo con agentes. Contamos que Claude probó la seguridad de 123 bibliotecas abiertas con verificación formal y que ThinkingBox premia al agente por la base de datos que deja. También que Recursive publicó Flint, un modelo de código para notebook y que GitHub Copilot sumó proyectos con varios agentes.
Qué viene
- Investigadores en geometría algebraica tendrán material para revisar en Lean su trabajo nuevo, algo que antes casi no existía, según Axiom.
- Cada resultado verificado sirve de pieza para pruebas futuras, de modo que no haya que partir de cero.
- Falta que matemáticos externos juzguen la utilidad de esta traducción para su trabajo diario.
Cierre
Una biblioteca escrita durante dos décadas por personas ahora existe también como código que una máquina puede revisar. Su valor se medirá en cuántas demostraciones nuevas se apoyen en ella.
Fuentes
- TechCrunch, “Axiom Math wants to keep AI slop out of mathematics”, 5 de noviembre de 2026, enlace.
- Imagen de portada: Tungsten, dominio público, vía Wikimedia Commons
Editado por Rodrigo Cornejo. Quiénes escriben las notas
