On August 18, 2026, Terence Tao announced on his blog the launch of Palomar (palomar-registry.org) — a registry of mathematics verified in the Lean type-checking language, which he himself describes as a “preprint server for Lean proofs.” The registry is open to submissions of snapshots of public repositories containing Lean proofs; the initiative was developed by Lean FRO and the ICARM research institute.

What happened

The scientific advisory board of the registry includes Tao, Jeremy Avigad, Matthew Ballard, Jaume de Dios, Nestor Guillen, Bryna Kra, Kim Morrison, Ravi Vakil, and Akshay Venkatesh. Palomar accepts snapshots of public GitHub repositories at a specific commit, containing Lean code: a challenge file with a readable statement, a solution module with a proof of any length, and a formalization.yaml file with an informal description, metadata, and disclosures. A snapshot is registered only after three automated checks without human involvement: the Comparator tool checks that the code passes type-checking and proves exactly the stated statement against a pinned version of Mathlib and a whitelist of allowed axioms, an independent LLM cross-checks the formal and informal statements, and a third level audits the disclosures in formalization.yaml. The first entry in the registry has already been registered — it is the proof of the Sendov conjecture with the identifier PALOMAR-2026-08-13-000001, whose formalization is attributed to Tao.

Context

Lean is a type-checking language that allows mathematical statements to be formalized as code and proofs to be checked mechanically, and the Mathlib library serves as the foundation against which proofs are checked in the registry. In format, Palomar is similar to a preprint server in the style of arXiv, but differs in its trust mechanism: before registration, the material undergoes machine checking, after which the result becomes a citable record with a unique identifier. The registry is explicitly not a journal: it separates “proof of the statement” from peer review, so the novelty and significance of the result are not part of the automated check. The context of the project's emergence is an avalanche of formalized AI proofs that are difficult for a non-specialist to verify: before the appearance of such a registry, a claim of a machine-checked proof was difficult to confirm without deep expertise in Lean code.

Why this matters for the industry

For the industry, Palomar is not a product, but an infrastructural standard of trust in machine-checked results: a reproducible verification protocol and a public citable dataset of verified theorems. For builders, this opens up a new surface — an end-to-end agentic workflow “formulated — formalized — submitted to the registry” and tooling around formalization: agents, pipelines, search, and integrations. The standardization signal is significant: the trust mechanism for machine-checked results is fixed at the top of the discipline (Tao, ICARM/NSF, Lean FRO), and future “AI-proof” products will be evaluated by the criterion of whether their result can be submitted to the registry. The dynamics of registered entries over time may become a public indicator of the growth of AI capabilities in theorem proving.

Why this matters for users

The registry is public and searchable, with filters by Mathlib, arXiv, and MSC: any reader can see which results have already passed verification. The Comparator tool and the standard formalization.yaml format are available for study, the submission instructions are public on the palomar-registry.org/how-to-submit page, and if desired, one can submit one's own Lean formalization. According to Tao, modern AI agents are good at helping with the mechanics of submission. Discussion of the registry is taking place in the Palomar channel on Lean Zulip.

What is still unknown / limitations

When reading the results of the registry, it is worth considering several caveats. The second level of verification — the correspondence between the formal and informal statement — is performed by an LLM, not a formal method, so a formalization error (the Lean statement being broader or narrower than the informal description) may pass the check. The input for the third level — the audit of disclosures in formalization.yaml — is the submitter's self-report, and how far the machine is able to verify the honesty of self-disclosure is not disclosed in the statement. A low barrier to entry scales the flow of AI-generated submissions, and the ease of submission itself is not a guarantee of the quality of the result.

Sources

Author

Look at AI, editorial team