Axiom Math verifica el Stacks Project para frenar el «slop» de la IA

Cómo funciona la verificación

Los matemáticos reescriben una demostración como código en el lenguaje Lean, y un asistente de demostración lo revisa línea a línea. Los ingenieros usan la misma idea, la verificación formal, para confirmar diseños de chips, e investigadores en Francia la emplearon para detectar errores en un software que calcula prestaciones familiares.

Stacks era una prueba difícil porque sus teoremas y definiciones dependen unos de otros, como un árbol genealógico. El matemático de Columbia Johan de Jong inició el proyecto de código abierto en 2005, y abarca desde álgebra universitaria hasta geometría algebraica y teoría de números. «Lo grande y lo delicado no van juntos», dijo la CEO, Carina Hong.

Axiom dio a sus agentes una jerarquía laxa y los dejó trabajar en paralelo, eligiendo sus propias tareas. La empresa también entrenó sus propios modelos matemáticos. Según Ashvin Swaminathan, la matemática formalizada tenía un «enorme agujero negro» en geometría algebraica, sobre el que ahora pueden construir los investigadores que usan Lean.

Más allá de las matemáticas

Axiom sostiene que cada resultado verificado es un bloque de construcción. Terence Tao lo resume así: «Cuantas más demostraciones formalizadas tienes, más puedes crear». Los desarrolladores también son público objetivo, pues garantizar un código sin errores ni fallos de seguridad se complica a medida que los agentes de IA escriben más software.

Hong, de 25 años, abandonó un doctorado en matemáticas en Stanford y fundó Axiom en marzo de 2025. En marzo cerró una Serie A de 200 millones de dólares liderada por Menlo Ventures. Además, retó abiertamente a las empresas de programación a trabajar en formalización a esta escala.