18 August, 2026 inadmin,advertising| Tags:Lean,Palomar| byTerence 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 thatPalomar registry of Lean verified mathematics, which is an initiative incubated by theLean FROand byICARM, is now open for submissions. I am serving in several roles on this registry, including on the scientific advisory board, together withJeremy Avigad,Matthew Ballard,Jaume de Dios,Nestor Guillen,Bryna Kra,Kim Morrison,Ravi Vakil, andAkshay Venkatesh.
A detailed motivation for Palomar can be foundhere, and further information about Palomar can be foundhere. 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 theastronomical 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
(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 toolComparator; 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. It is worth stressing that the checks in (a) and (b) fall well short of what a proper human peer review of a submission for novelty, interest, and accuracy would give; in particular, Palomar isnota peer-reviewed journal.
The submission process is thorough, but achievable: as a test, Isuccessfully managedto submit my ownrecent formalization of the proof of Sendov’s conjectureto 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 (whether human-generated, AI-generated, or some mixture of both) are welcome; please read the (somewhat detailed) instructionsherebefore starting a submission. (I will however note that modern AI 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 onthis Zulip channel.
To enter in LaTeX in comments, use $latex$ (without the signs, of course; in fact, these signs should be avoided as they can cause formatting errors). Also, backslashes \ need to be doubled as \\. See theabout pagefor details and for other commenting policy.
Blog at WordPress.com.Ben Eastaugh and Chris Sternal-Johnson.