Axiom Math quiere mantener la basura de IA fuera de las matemáticas

Axiom Math, una startup valorada en 1.600 millones de dólares, ha verificado formalmente el Proyecto Stacks—una de las mayores bibliotecas matemáticas escritas por humanos—traduciendo sus 7.654 páginas a aproximadamente 16 millones de líneas de código Lean verificado por computadora mediante agentes de IA. La verificación formal, similar a los métodos usados en diseño de chips y depuración de software, asegura la solidez lógica al hacer que un asistente de pruebas revise cada línea. El Proyecto Stacks, iniciado en 2005 por Johan de Jong, abarca álgebra, geometría y teoría de números, y sus teoremas interconectados plantearon un desafío significativo para los agentes de Axiom, que trabajaron en paralelo bajo una jerarquía flexible y fueron entrenados para desarrollar criterio matemático. El logro llena un vacío importante en la geometría algebraica formalizada y proporciona una base verificada y reutilizable para futuras pruebas y software generado por IA, abordando las preocupaciones sobre la "basura de IA" al permitir que los agentes construyan sobre matemáticas confiables en lugar de empezar desde cero.

(Fuente：TechCrunch)