Terry Tao launches Palomar, a preprint-style registry for Lean-verified proofs

As AI systems churn out more mathematical proofs — many of them formalized in the Lean proof assistant — a practical problem has emerged: confirming that a given Lean repository actually proves what it claims. Doing so requires checking that the formal statements typecheck, that the proof sneaks in no extra axioms or shortcuts, and that the formal claim genuinely corresponds to the informal result being advertised. That verification is hard for anyone who isn’t a Lean expert. Palomar, a new registry incubated by the Lean FRO and ICARM and now open for submissions, aims to close that gap. Terry Tao, who sits on its scientific advisory board alongside mathematicians including Jeremy Avigad, Bryna Kra, Ravi Vakil, and Akshay Venkatesh, describes it as roughly a preprint server for Lean proofs.

Mechanically, Palomar catalogs snapshots of external GitHub repositories pinned to specific commits. Each submission must follow current formalization best practices: a short human-readable ‘challenge file’ stating the claimed results in Lean, a ‘solution module’ containing the full proof, and a ‘formalization.yaml’ with an informal description plus metadata and disclosures. Submissions face two gates. The first is deterministic — the Lean tool Comparator confirms the solution typechecks and proves exactly the challenge’s claims. The second is not: a large language model judges whether the informal description matches the formal statement. Passing both earns a registry entry.

Tao is careful to frame the limits. These checks fall well short of human peer review for novelty, interest, or correctness, and Palomar is explicitly not a journal. It accepts human-authored, AI-authored, or hybrid formalizations, and Tao notes that AI agents are useful for the mechanical parts of submission — though he still recommends human oversight. As a test, he successfully registered his own formalization of Sendov’s conjecture. The registry signals a broader push to build trustworthy infrastructure around machine-checked mathematics at a moment when the volume of AI-generated proofs is rising faster than the community’s ability to vet them.