El matemático Terence Tao anunció la apertura de Palomar, un registro de demostraciones matemáticas verificadas en el lenguaje de pruebas Lean, una iniciativa impulsada por Lean FRO e ICARM. El proyecto surge ante la proliferación de pruebas generadas por inteligencia artificial, algunas formalizadas en Lean, y la dificultad de comprobar que un repositorio realmente demuestra lo que afirma. Para superar esa barrera, Palomar exige a cada repositorio un archivo de enunciado, un módulo con la demostración y un fichero formalization.yaml con la descripción informal y metadatos. Un sistema automático, llamado Comparator, verifica que el código compila y prueba exactamente lo declarado, mientras un modelo de lenguaje grande evalúa la coherencia entre la descripción informal y el enunciado formal. Si pasa ambas revisiones, el repositorio queda registrado con un identificador estable asociado a un commit concreto de GitHub. Tao subraya que Palomar no equivale a una revista con revisión por pares: no evalúa novedad ni interés. Como prueba, el propio Tao registró su formalización reciente de la conjetura de Sendov. El registro ya admite envíos de resultados clásicos y nuevos, generados por personas, por IA o de forma mixta, y la discusión se canaliza en un canal de Zulip.
Noticias agregadas con IA