Palomar: registro aberto de matemática verificada em Lean

Um registro para provas formalizadas

O Palomar, registro de matemática verificada em Lean, abriu inscrições para repositórios externos do GitHub que contenham formalizações de resultados matemáticos. A iniciativa foi incubada pela Lean FRO e pela ICARM e pretende funcionar, em uma primeira aproximação, como um servidor de preprints para provas em Lean, organizando versões específicas dos repositórios a partir de um commit do GitHub.

A criação do registro responde à proliferação recente de provas geradas por inteligência artificial e formalizadas em Lean. Para avaliá-las, é necessário verificar se as afirmações formais realmente têm provas que compilam, se não utilizam recursos considerados “trapaças”, como axiomas adicionais, e se correspondem semanticamente às descrições informais dos resultados. Essa tarefa pode ser difícil para pessoas que não são especialistas em Lean.

Como funciona a verificação

Cada repositório submetido deve seguir práticas atuais de formalização e incluir, entre outros requisitos técnicos, três componentes centrais: um “challenge file”, com uma descrição curta e legível dos resultados em Lean; um “solution module”, que contém a prova, de extensão arbitrária; e um arquivo formalization.yaml, que descreve os resultados em linguagem informal e registra metadados e declarações relevantes.

O Palomar realiza duas verificações principais. A primeira confirma mecanicamente, com a ferramenta Lean Comparator, que o módulo de solução compila e prova exatamente os resultados declarados no arquivo de desafio. A segunda avalia, de modo não determinístico e com um modelo de linguagem, se a descrição informal no formalization.yaml parece corresponder ao enunciado formal. O registro também verifica padrões mínimos exigidos para uma entrada.

A aprovação, porém, não equivale a uma revisão acadêmica completa. O texto ressalta que esses procedimentos ficam muito aquém de uma avaliação humana de novidade, interesse e correção; o Palomar não é um periódico com revisão por pares. O processo de submissão é descrito como detalhado, mas viável, e uma revisão humana continua sendo fortemente recomendada, embora agentes modernos de IA possam ajudar nos aspectos mecânicos.

Primeiras submissões e escopo

Como teste, Terence Tao submeteu com sucesso ao registro sua formalização recente da prova da conjectura de Sendov e pretende enviar outras formalizações mais antigas. O Palomar aceita trabalhos sobre resultados antigos ou novos, produzidos por humanos, por IA ou por uma combinação dos dois. As discussões e os comentários sobre a iniciativa ocorrerão em um canal do Zulip. A proposta, portanto, é oferecer uma camada organizada de verificação técnica e correspondência semântica para provas em Lean, sem substituir o julgamento humano necessário à avaliação matemática mais ampla.