Palomar – a registry of Lean verified mathematics

The Palomar registry of Lean verified mathematics, incubated by the Lean FRO and ICARM, is now open for submissions, aiming to serve as a preprint server for Lean proofs by checking that formalized statements match informal claims. The registry's checks include a mechanical verification using the Lean tool Comparator and a non-deterministic review by a large language model, but it is not a peer-reviewed journal. Terence Tao, a member of the scientific advisory board, successfully submitted his formalization of the proof of Sendov's conjecture as a test.

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 https://palomar-registry.org/ , which is an initiative incubated by the Lean FRO https://lean-lang.org/fro/ and by ICARM https://icarm.io/ , is now open for submissions. I am serving in several roles on this registry, including on the scientific advisory board, together with Jeremy Avigad https://www.andrew.cmu.edu/user/avigad/ , Matthew Ballard https://www.matthewrobertballard.com/ , Jaume de Dios https://jaume.dedios.cat/ , Nestor Guillen https://www.ndguillen.com/ , Bryna Kra https://en.wikipedia.org/wiki/Bryna Kra , Kim Morrison https://tqft.net/ , Ravi Vakil https://math.stanford.edu/~vakil/ , and Akshay Venkatesh https://www.math.ias.edu/~akshay/ . A detailed motivation for Palomar can be found here https://palomar-registry.org/statement , and further information about Palomar can be found here https://palomar-registry.org/about . 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 https://sites.astro.caltech.edu/palomar/homepage.html 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 https://github.com/mathlib-initiative/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 https://github.com/leanprover/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. 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 is not a peer-reviewed journal. The submission process is thorough, but achievable: as a test, I successfully managed https://palomar-registry.org/entry?id=PALOMAR-2026-08-13-000001&version=1 to submit my own recent formalization of the proof of Sendov’s conjecture https://github.com/teorth/sendov 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 whether human-generated, AI-generated, or some mixture of both are welcome; please read the somewhat detailed instructions here https://palomar-registry.org/how-to-submit before 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 on this Zulip channel https://leanprover.zulipchat.com/ narrow/channel/621638-Palomar .