Announcing the Palomar Registry

Today we're launching the Palomar Registry, an index of formalized mathematics repositories with a valid #comparator setup and #formalization.yaml metadata. Limited automatic review rejects submissions with obvious discrepancies between the informal and formal statements, and errors in the metadata.

This is jointly incubated by the Lean FRO and ICARM, and the initial advisory board consists of Jeremy Avigad, Matthew Ballard, Jaume de Dios, Nestor Guillen, Bryna Kra, Kim Morrison, Terence Tao, Ravi Vakil and Akshay Venkatesh.

Please read our Palomar Statement, explaining the motivation behind this registry, and our About page to understand the mechanism. Terry has also written about Palomar on his blog.

Palomar doesn't have any opinions about use of AI: there are already entries ranging from no-AI-at-all to autonomously formalized. What we do expect is that this is explained clearly in your #formalization.yaml file.

If you have a repository with at least one of a #comparator setup or a #formalization.yaml metadata, we'd encourage you to fulfill the requirements and submit. You can find detailed instructions at https://palomar-registry.org/how-to-submit, or just get started at https://submit.palomar-registry.org/ (it's a fairly interactive process that should help you identify problems with your submission: bug reports are very welcome). (There's also an llms.txt if you'd like to have an agent help you submit.)

There is a new public Zulip channel #Palomar for discussion. You can link to individual entries from Zulip using the identifiers: PALOMAR-2026-08-13-000001, and link to the main page using #palomar.

(Oh, and please reply to all future announcements of maths results on social media with "But is it on Palomar?" :-)