Announcing Palomar, a registry of Lean verified mathematics
Palomar, a public registry of Lean formalizations whose proofs have been machine-checked, is now open for submissions. Incubated by ICARM together with the Lean FRO, it gives formalized results a durable, citable record after three automated checks of the proof, the statement, and the submission's disclosures.
ICARM is pleased to announce Palomar, a public, searchable registry of Lean formalizations whose proofs have been machine-checked. Formalized mathematics is growing quickly, but much of it remains scattered across repositories, announcements, and private links. Palomar aims to organize this by collecting entries that point to immutable snapshots of public repositories. Palomar also records the exact statement that was checked, its dependencies and pinned Lean toolchain, the outcome of the proof check, and the findings of an automated review.
An entry is only registered after three automated checks find no blocking problem: the Lean tool Comparator verifies that the proof proves the recorded statement against a specified version of Mathlib using only permitted axioms; a language model judges whether the formal statement is a fair rendering of the informal claim and clears Palomar's minimum standard; and a third check audits the required disclosures in the submission's formalization file. All three run automatically, and involve no human editorial step.
Palomar was incubated by the Lean FRO and ICARM, together with its initial scientific advisory board, which consists of ICARM directors Jeremy Avigad and Matthew Ballard, as well as Jaume de Dios, Nestor Guillen, Bryna Kra, Kim Morrison, Ravi Vakil, and Akshay Venkatesh. Tao announced the opening of the registry on his blog, and discussion is taking place on the Palomar channel of the Lean Zulip.
Palomar is the kind of infrastructure ICARM is here to support: it helps mathematicians take advantage of new technologies for mathematical reasoning while keeping the mathematics itself central, independently auditable, and publicly accessible. We will continue to push on efforts like this as new opportunities arise.