Terence Tao and Board Launch Palomar Registry to Standardize Lean-Verified Math
The new public record aims to combat unvetted AI-generated claims by providing a durable, indexable baseline for machine-assisted proofs.
Terence Tao and a board of prominent mathematicians have launched Palomar, a public registry for Lean-verified mathematical formalizations. The platform establishes a durable, indexable record for machine-assisted proofs to ensure they meet rigorous technical and transparency standards.
Incubated by the Lean Focused Research Organization (Lean FRO) and the Institute for Computational Analysis of Research Mathematics (ICARM), Palomar functions as a specialized archive. Terence Tao described the registry as a "zeroth approximation" of a preprint server, similar to arXiv, but specifically for Lean proofs. To maintain these standards, the registry requires submissions to utilize "comparator" technology to separate theorem statements from proofs, a "formalization.yaml" file for metadata and provenance, and "Verso" for documentation rendering.
The Crisis of Machine-Generated Proofs
The initiative arrives as Large Language Models (LLMs) increasingly generate mathematical proofs. While the Lean proof assistant can verify these outputs, auditing a repository to ensure a proof is legitimate—and does not rely on "cheats" such as adding extra axioms—remains difficult for non-experts. This has created a widening gap between the volume of machine-generated claims and the mathematical community's capacity to vet them.
According to the Palomar Founding Statement, the rapid increase in such announcements is "generating confusion, while also eroding our current standard for what constitutes an ‘established mathematical fact.’"
Establishing a Baseline
Palomar aims to solve this by automating the verification of mechanical correctness. The registry employs a mechanical check via Comparator to ensure that a proof typechecks. However, the registry explicitly states that inclusion in Palomar does not constitute a certification that the verified formal statement matches the original informal description.
By establishing a community-accepted minimum standard for "baseline contributions," Palomar allows traditional peer-reviewed journals to shift their focus. Rather than spending resources on basic logical grinding, reviewers can prioritize conceptual novelty and elegance, knowing the mechanical correctness has already been indexed.
Governance and Oversight
The registry is overseen by a Scientific Advisory Board comprising several leading figures in the field, including Jeremy Avigad, Matthew Ballard, Jaume de Dios, Nestor Guillen, Bryna Kra, Kim Morrison, Terence Tao, Ravi Vakil, and Akshay Venkatesh.
As the volume of AI-assisted mathematics continues to grow, the industry will be watching whether Palomar can successfully serve as the primary filter for formalizations before they reach the stage of traditional academic publication.