HERRAMIENTAS
Palomar abre un registro para verificar pruebas en Lean y acotar afirmaciones de IA en matemáticas
Palomar abre envíos como registro de instantáneas de GitHub con pruebas formales en Lean, verificadas mecánicamente y contrastadas con descripciones informales mediante un modelo de lenguaje. Anunciado por Terence Tao, el sistema crea un rastro auditable sin hacer de árbitro científico. Útil para evaluar el auge de pruebas generadas con IA.
Qué ha ocurrido
El 18 de agosto se abrió Palomar, un registro público que vincula pruebas formales en Lean a commits fijos de GitHub. Cada envío incluye Challenge.lean (enunciado), Solution.lean (prueba) y formalization.yaml (descripción y metadatos). Un verificador (Comparator) comprueba que la solución demuestra el reto, y un modelo de lenguaje evalúa si la descripción informal parece corresponder al resultado. El registro crea un artefacto indexable y una trazabilidad, pero no actúa como revisión por pares ni certifica novedad o importancia.
Qué significa para creadores
Si cubres IA y matemáticas, cita el registro de Palomar y el commit exacto al informar sobre resultados en Lean o generados con IA. Explica claramente que Palomar valida mecánicamente la correspondencia entre reto y solución y que la comprobación con modelo de lenguaje puede fallar; no es un aval experto. Úsalo como base para piezas didácticas: muestra dónde leer Challenge.lean, Solution.lean y formalization.yaml, qué se ha verificado y qué sigue requiriendo juicio humano.
Fuente y contexto
Según RuntimeWire, el anuncio corrió a cargo de Terence Tao, uno de los cuatro mantenedores técnicos iniciales junto a Matthew Ballard, Nestor Guillen y Jaume de Dios Pont. El proyecto fue incubado por Lean Focused Research Organization y el Institute for Computer-Aided Reasoning in Mathematics, y cuenta con un consejo asesor que incluye a Jeremy Avigad, Bryna Kra, Kim Morrison, Ravi Vakil y Akshay Venkatesh. Palomar actualmente admite Lean, acepta envíos humanos, de IA o mixtos, y usa revisión automatizada; los materiales no confirman una moderación humana separada.