Llegaron tantas demostraciones escritas por máquinas que los matemáticos han montado una oficina de registro — y uno de sus dos controles lo hace un modelo de lenguaje

Terence Tao anunció el 18 de agosto que Palomar, un registro de matemáticas verificadas en Lean incubado por la Lean FRO y por ICARM, ya acepta envíos. El problema que lo motiva es reciente: en los últimos meses ha aparecido un gran número de demostraciones generadas por IA de resultados viejos y nuevos, y buena parte de ellas se han formalizado en Lean, el asistente de pruebas que permite a una máquina confirmar cada paso. Pero un repositorio de Lean alojado en GitHub no se explica solo. Averiguar si el código demuestra lo que su autor dice que demuestra es trabajo de verdad, y resulta casi imposible para un matemático que no usa Lean. Palomar somete cada repositorio a dos controles. El primero es mecánico: una herramienta de Lean llamada Comparator confirma que el módulo pasa la comprobación de tipos y demuestra exactamente los resultados anunciados. El segundo pregunta si la descripción en lenguaje corriente coincide con el enunciado formal, y de ese se encarga un modelo de lenguaje grande. Los repositorios que superan ambos quedan registrados, y se publican junto a ellos el enunciado exacto, las bibliotecas empleadas y los comentarios de la revisión. Tao lo describe como el equivalente de un servidor de preprints para demostraciones en Lean, y forma parte de un consejo asesor científico con Jeremy Avigad, Matthew Ballard, Jaume de Dios, Nestor Guillen, Bryna Kra, Kim Morrison, Ravi Vakil y Akshay Venkatesh.

✓ Verificado · 4 fuentes

Noticias relacionadas