Axiom Math dice que sus agentes de IA verificaron formalmente el Stacks Project
🎧 Escucha esta noticia
Axiom Math anunció que sus agentes de IA verificaron formalmente el Stacks Project, una referencia de código abierto que reúne resultados de álgebra, geometría y teoría de números. Según TechCrunch, el equipo tradujo unas 7.654 páginas a cerca de 16 millones de líneas de código en el lenguaje Lean, revisadas línea por línea por un asistente de pruebas.
La empresa dice que organizó a los agentes para trabajar en paralelo mientras preservaban las conexiones entre teoremas y definiciones interdependientes. La directora ejecutiva Carina Hong dijo a TechCrunch que Axiom entrenó sus propios modelos para matemáticas y que el resultado cubre una brecha especialmente grande en la formalización de la geometría algebraica, donde, según la empresa, los investigadores que usaban Lean tenían antes poco material en el que apoyarse.
Por qué importa · interpretación editorial
Si se confirma la afirmación de Axiom Math, la formalización podría dar a investigadores que usan Lean una base mucho mayor para trabajar en geometría algebraica, un área en la que la empresa dice que había poco material formalizado. El caso también ilustra cómo agentes paralelos pueden manejar dependencias en proyectos matemáticos extensos.
Fuentes
InvestigaciónAgentes