IA de Facebook formaliza libros de matemáticas

Investigadores de Facebook IA han desarrollado un sistema llamado RepoProver, capaz de formalizar automáticamente libros de texto matemáticos utilizando inteligencia artificial. El sistema, cuyo código está disponible en GitHub, emplea una arquitectura multi-agente que colabora en un repositorio Git con el proyecto Lean, un lenguaje de programación formal. Los agentes se dividen en 'sketcher' (para traducir definiciones y teoremas), 'prover' (para completar las pruebas) y 'reviewer' (para asegurar la calidad). RepoProver ha sido utilizado para formalizar el libro de texto de álgebra combinatoria de Darij Grinberg, demostrando su capacidad para automatizar tareas complejas en matemáticas. El sistema requiere Python 3.10+ y una configuración inicial que incluye la creación de un proyecto Lean con Mathlib, archivos LaTeX organizados por temas, un archivo manifest que define los objetivos de formalización, un rastreador de problemas y un repositorio Git. Se pueden ejecutar múltiples agentes en paralelo y el sistema permite la ejecución distribuida en varios ordenadores. Facebook IA ha proporcionado ejemplos y herramientas para analizar el uso de tokens y la eficiencia de los agentes, facilitando la comprensión y el desarrollo del sistema.