Palomar Registry Launches as a Preprint Server for Lean‑Verified Mathematics

Palomar provides a lightweight, automated gatekeeper for Lean formalizations

Palomar is a new registry that accepts snapshots of GitHub repositories containing Lean code, checks that the formal statements type‑check, and uses a large language model to compare informal descriptions with the claimed results. The mechanical check (using the Lean tool Comparator) guarantees logical correctness, while the AI check offers a non‑deterministic sanity test of the informal claim. Palomar explicitly does not perform human peer review of novelty or interest, mirroring the arXiv’s minimal acceptance criteria.

Submission workflow is intentionally rigorous yet achievable

A submission must include:

A challenge file with a concise, human‑readable Lean statement of the theorem(s).
A solution module containing the full Lean proof.
A formalization.yaml file that supplies an informal description, metadata, and disclosures.

Tao demonstrated the process by successfully registering his own formal proof of Sendov’s conjecture. The registry accepts contributions from humans, AI agents, or hybrids, and modern AI assistants can help with the mechanical aspects of the submission.

Community reaction highlights strengths and concerns

"The second check (b) is non‑deterministic, being performed by a large language model. Shouldn’t this be just preliminary? I think submissions should have an additional, human‑performed level of verification." – Anonymous comment

"We do not have the resources to host and maintain repositories directly, but would be open to expanding the whitelist of approved repository hosting services beyond Github if there is sufficient demand for doing so." – Terence Tao

"A very quick look at Palomar suggests that it would be much more helpful if each submission required (a) a meaningful Title, and (b) a (well‑written) Abstract explaining what is proved — just as one sees in arXiv." – David Bevan

"Palomar will definitely be something we integrate for data checks and validation" – ygtisik (author of a registry of AI usage in science).

These comments illustrate three recurring themes:

Verification depth – some users want a human layer of review beyond the automated checks.
Repository hosting – reliance on GitHub is seen as a single point of failure; expanding to other forges is desirable.
Metadata quality – clearer titles and abstracts would improve discoverability, similar to arXiv conventions.

Technical design choices and trade‑offs

GitHub‑centric model – simplifies identity, spam control, and versioning, but creates a dependency on a single service. As noted by several commenters, future extensions could whitelist alternative git forges.
AI‑driven semantic check – provides a scalable way to flag mismatches between formal statements and informal descriptions, yet remains non‑deterministic. The registry treats this as a preliminary filter, not a definitive judgment.
Minimal human involvement – mirrors arXiv’s approach, allowing the system to scale to the anticipated volume of Lean formalizations without a dedicated review team.

Why mathematicians might contribute

Visibility – entries appear in a searchable registry, giving credit to authors and exposing formalizations to the broader community.
Reusability – a verified Lean proof can be imported into other projects, reducing duplication of effort.
AI ecosystem support – the registry supplies high‑quality, machine‑checkable data that can train or evaluate AI proof assistants.
Community standards – participating helps shape best‑practice conventions for Lean formalizations.

Comparison with existing efforts

TheoremDB and Metamath already provide searchable databases of formal proofs, but Palomar focuses specifically on Lean and integrates automated type‑checking plus AI‑based semantic validation.
Isabelle AFP offers a long‑standing archive for Isabelle/HOL; Palomar can be seen as Lean’s analogue, though still in early stages.

Outlook and open questions

Human‑level validation – third‑party services could layer peer review on top of Palomar’s minimal checks.
Metadata enhancements – adding explicit title and abstract fields to formalization.yaml would align entries with scholarly preprint norms.
Hosting diversification – expanding beyond GitHub would mitigate reliance on a single platform and accommodate users on alternative forges.
Incentive structures – the community is still exploring what motivates contributions beyond reputation and the desire for reusable formalizations.

Palomar is now open for submissions. Detailed instructions are available at the registry’s how‑to‑submit page, and discussion continues on the dedicated Lean Zulip channel.