Palomar: um registro de matemática verificada em Lean
Palomar: A registry of Lean verified mathematics
O registro Palomar, incubado pela Lean FRO e pela ICARM, está aberto para submissões de provas formalizadas em Lean. Ele verifica que os repositórios do GitHub provam exatamente o que afirmam, usando o Comparator para checagem mecânica e um modelo de linguagem para validar a descrição informal. Terence Tao, membro do conselho consultivo, já submeteu sua formalização da conjectura de Sendov. O registro não é um periódico revisado por pares, mas um análogo de servidor de preprints para provas Lean.
O primeiro check (a) é puramente mecânico, usando a ferramenta Comparator do Lean; o segundo check (b) é não determinístico, sendo realizado por um grande modelo de linguagem.