Palomar: un registro de matemáticas verificadas con Lean
Palomar: A registry of Lean verified mathematics
Terence Tao anuncia la apertura de Palomar, un registro de repositorios de GitHub con código Lean que verifican teoremas matemáticos. El registro comprueba automáticamente que las pruebas compilan y que no contienen axiomas adicionales, y usa un modelo de lenguaje para validar que la descripción informal coincida con el resultado formal. Tao, miembro del consejo asesor, ya ha enviado su formalización de la conjetura de Sendov.
Una aproximación cero de lo que Palomar pretende ser es el análogo de un servidor de preprints para pruebas en Lean.