Palomar: el registro de pruebas Lean verificadas por IA
Un registro para las pruebas matemáticas verificadas por IA Terry Tao, uno de los matemáticos más influyentes del mundo, anunció el pasado 18 de agosto la apertura del Palomar registry, un nuevo registro público para pruebas formales escritas en Lean — el lenguaje de verificación matemática que se ha convertido en el estándar de facto …









