Jueves 5 de noviembre de 2026 ·

Axiom Math formaliza en Lean el Stacks Project, unas 7.500 páginas de matemáticas, como base verificable para agentes de IA

Relevancia 78 de 100 Estados Unidos, California

La startup Axiom Math afirma haber convertido el Stacks Project, una referencia matemática abierta de unas 7.500 páginas, en unos 16 millones de líneas de código Lean verificadas por ordenador. Usó agentes de IA que trabajaron en paralelo, eligiendo sus propias tareas dentro de una jerarquía. La empresa propone esta biblioteca como base para nuevas demostraciones y para el software que escriban los agentes.

Qué significa

Los agentes de IA podrán construir demostraciones y software sobre resultados ya comprobados por un verificador formal, en lugar de hacerlo sobre afirmaciones sin revisar. La formalización a esta escala convierte el corpus en un activo reutilizable que facilita los trabajos posteriores, especialmente en geometría algebraica, donde había muy poco material.

Fuentes originales

Resumen de Hoy en IA. Pulsa una fuente para leer la noticia completa en su idioma original.

También ese día

Todas las noticias de IA del jueves 5 de noviembre de 2026 ->