Palomar: um registro de matemática verificada em Lean

Foi anunciado o Palomar, repositório aberto que coleta e organiza demonstrações formais escritas na linguagem de prova Lean.

Confirmado

A existência do registro, sua disponibilidade pública e a intenção de agregar contribuições da comunidade. Anunciado por Terry Tao em seu blog.

Ainda incerto

O ritmo de crescimento da biblioteca e a abrangência das áreas cobertas inicialmente.

Por que importa

Centralizar provas formais facilita a reutilização de resultados e acelera a pesquisa em matemática formalizada.