Investigadores han presentado 'Lean Collab', un nuevo sistema colaborativo para la demostración de teoremas utilizando Lean 4 y la red neuronal Ensue. La herramienta busca acelerar la verificación formal, permitiendo que múltiples agentes trabajen en la resolución de problemas matemáticos complejos de manera concurrente. Para su uso, requiere la instalación de Lean, Mathlib y Rust, además de una clave API de Ensue. El sistema funciona a través de un plugin que se instala y configura, definiendo parámetros como el identificador del teorema, la URL de la API de Ensue y el número máximo de agentes paralelos. Un componente clave es el 'warm server', que pre-carga Mathlib en memoria para reducir significativamente el tiempo de verificación de tácticas. La herramienta utiliza Claude, un asistente de IA, para orquestar el proceso de demostración, coordinando a los agentes y componiendo la prueba final. Los usuarios deben ser conscientes del consumo de tokens de API, especialmente al utilizarlos.
Noticias agregadas con IA