Palomar: Nuevo Registro para la Verificación de Matemáticas en Lean

Se ha lanzado Palomar, un registro destinado a la verificación de matemáticas formalizadas en el lenguaje Lean, una iniciativa impulsada por Lean FRO e ICARM. Este registro busca facilitar la validación de pruebas generadas por inteligencia artificial y por humanos, asegurando que las afirmaciones en Lean sean correctas y que las pruebas no contengan errores. El proceso de envío está diseñado para ser riguroso, permitiendo la inclusión de resultados tanto antiguos como nuevos, y se espera que contribuya a la claridad en la comunidad matemática.