Palomar: A registry of Lean verified mathematics

Palomar is a registry for Lean-verified mathematics that stores snapshots of GitHub repositories containing a challenge file, a solution module, and a formalization.yaml metadata file. Submissions are automatically type-checked, verified against the challenge, and reviewed for consistency between informal description and formal statement using Lean’s Comparator and an LLM reviewer. The registry is overseen by a scientific advisory board that includes Jeremy Avigad, Bryna Kra, Ravi Vakil, among others, and accepts both human- and AI-generated formalizations.