Palomar – a registry of Lean verified mathematics | What's new
What's new Updates on my research and expository papers, discussion of open problems, and other maths-related topics. By Terence Tao
Home
About
Career advice
On writing
Books
Mastodon+
Applets
Subscribe to feed
Palomar – a registry of Lean verified mathematics
18 August, 2026 in admin, advertising | Tags: Lean, Palomar | by Terence Tao
In recent months there has been a proliferation of AI-generated proofs of various old and new results, some of which have been formalized in the proof assistant language Lean. However, checking that a given Lean repository actually proves the claimed statement is somewhat non-trivial, especially for an audience which is not expert in the use of Lean: one has to first check that the claimed formal Lean statements have proofs that typecheck, that the proofs do not contain any "cheats" such as adding additional axioms, and that the formal statements also match (in a semantic sense) the informal description of the claimed results.
To help bring some clarity to this situation, I am happy to announce that Palomar registry of Lean verified mathematics, which is an initiative incubated by the Lean FRO and by ICARM, is now open for submissions. I am serving in several roles on this registry, including on the scientific advisory board, together with Jeremy Avigad, Matthew Ballard, Jaume de Dios, Nestor Guillen, Bryna Kra, Kim Morrison, Ravi Vakil, and Akshay Venkatesh.
A detailed motivation for Palomar can be found here, and further information about Palomar can be found here. A zeroth approximation of what Palomar intends to be is the analogue of a preprint server for Lean proofs. More precisely, Palomar (which is named after the astronomical observatory) is a registry of external Github repositories (or more precisely, "snapshots" of such repositories, as represented by a specific Github commit) containing Lean code adhering to the current best practices for such formalizations, in particular containing
A "challenge file" containing a short, human readable description in Lean of the results claimed.
A "solution module" containing an (arbitrarily long) proof of the results claimed in the challenge file.
A "formalization.yaml" file describing the results in informal language, and also containing a number of other relevant metadata and disclosures.
(There are also some additional technical requirements for the repository which I will omit here.) If a snapshot of a repository is submitted to Palomar, it will check both (a) that the solution module typechecks and proves exactly the results claimed in the challenge file, and that (b) the informal description of the result in the formalization.yaml file appears to match the result claimed in the challenge file, and that the repository meets various minimal standards required for a registry entry. The first check (a) is purely mechanical, using the Lean tool Comparator; the second check (b) is non-deterministic, being performed by a large language model. If a repository passes both checks, it can be registered on Palomar.
The submission process is thorough, but achievable: as a test, I successfully managed to submit my own recent formalization of the proof of Sendov’s conjecture to Palomar, and also plan to submit some older formalizations to the registry soon.
In any event, the registry is now open for formalizations of both old and new results. Submissions are welcome; please read the (somewhat detailed) instructions here before starting a submission. (I will however note that modern agents are quite helpful in assisting with the mechanical details of the submission, though a human review is still strongly recommended.)
Discussion and feedback on Palomar will occur on this Zulip channel (which should be opened up to the public very shortly).
Share this:
Print (Opens in new window)<br>Print
Email a link to a friend (Opens in new window)<br>Email
More
Share on X (Opens in new window)
Share on Facebook (Opens in new window)<br>Facebook
Share on Reddit (Opens in new window)<br>Reddit
Share on Pinterest (Opens in new window)<br>Pinterest
Like Loading...
Recent Comments
Terence Tao on Notes on the classification of…Anonymous on A digestion of the Jacobian co…Anonymous on Notes on the classification of…Karim Adiprasito on A digestion of the proof of Se…Anonymous on A digestion of the proof of Se…Anonymous on Notes on the classification of…Anonymous on The blue-eyed islanders puzzle…dutifullyb3c31ab42c on A digestion of the proof of Se…Anonymous on A digestion of the proof of Se…Anonymous on Career adviceTeng Zhang on A digestion of the proof of Se…Teng Zhang on A digestion of the proof of Se…Teng Zhang on A digestion of the proof of Se…Anonymous on A digestion of the Jacobian co…Teng Zhang on A digestion of the proof of Se…
Top Posts<br>A digestion of the proof of Sendov's conjecture<br>A digestion of the Jacobian conjecture counterexample<br>Career advice<br>On...