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. 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 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 (whether human-generated, AI-generated, or some mixture of both) are welcome; please read the (somewhat detailed) instructions here 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.

The Polymath Blog

Polymath News and AI and at a later stage to consider resources and tools that can advance such projects. Tim Gowers recently proposed […]")
Polymath projects 2021 Following the post and separate posts describing some of […]")
A sort of Polymath on a famous MathOverflow problem
Ten Years of Polymath
Updates and Pictures by Bucić, Kwan, Pokrovskiy, and Sudakov First, there is a remarkable development on Rota’s basis conjecture (Polymath12) described in the paper Halfway to Rota’s basis conjecture, by Matija Bucić, Matthew Kwan, Alexey Pokrovskiy, and Benny Sudakov Abstract: In 1989, Rota made the following conject […]")
Polymath proposal: finding simpler unit distance graphs of chromatic number 5, defined as the minimum number of colours that can be assigned to the points of the plane so as to prevent any two points unit distance apart from being the same colour. It was first posed in 1950 and the bounds […]")
A new polymath proposal (related to the Riemann Hypothesis) over Tao’s blog A new polymath proposal over Terry Tao’s blog who wrote: “Building on the interest expressed in the comments to this previous post, I am now formally proposing to initiate a “Polymath project” on the topic of obtaining new upper bounds on the de Bruijn-Newman constant . […]")
Spontaneous Polymath 14 – A success!")
Polymath 13 – a success!
Non-transitive Dice over Gowers’s Blog is now running over Gowers blog. (Here is the link to the first post.) ")

15 comments

Comments feed for this article

18 August, 2026 at 10:42 pm

Anonymous

cool

18 August, 2026 at 10:50 pm

Anonymous

\> the second check (b) is non-deterministic, being performed by a large language model

Shouldn’t this be just preliminary? I think submissions should have an additional, human-performed level of verification.

19 August, 2026 at 6:09 am

Terence Tao

As stated above, Palomar does not perform human review of repositories, which will not scale to the volume of repositories we envisage processing. (This is similar to the arXiv, which performs minimal checks of acceptability for the preprints it accepts, but also does not perform human review.) However, we would be fine with a third-party service performing additional review on top of the minimal checks that Palomar performs.

19 August, 2026 at 1:04 am

Anonymous

As GitHub is becoming less reliable every year, have you considered alternate git forges or hosting the repositories yourself instead of relying on external companies to keep their services available in the future?

19 August, 2026 at 6:16 am

Terence Tao

We do not have the resources to host and maintain repositories directly, but would be open to expanding the whitelist of approved repository hosting services beyond Github if there is sufficient demand for doing so.

19 August, 2026 at 1:47 am

David Bevan

A very quick look at Palomar suggests that it would be much more helpful if each submission required (a) a meaningful Title, and (b) a (well-written) Abstract explaining what is proved — just as one sees in arXiv. At present, the titles and descriptions do not enable me to understand what many of the submissions achieve.

To be honest, I’m rather shocked that this went live without a requirement of this sort. (Who is the main interface actually supposed to be for if it’s impossible to work out what entries are about?)

19 August, 2026 at 6:24 am

Terence Tao

I’ll pass this suggestion on to the maintainers. Currently we rely on the \`project.name\` and \`project.description\` fields of the repository \`formalization.yaml\` to provide the informal description of the project, although this does not perfectly map on to the title and abstract of a preprint because the claims being registered may only form a subset of the content of the repository, rather than represent the full repository project itself. So there may be a need to add separate title and abstract fields, but this will need some discussion to implement properly.

19 August, 2026 at 2:07 am

Anonymous

Such a good idea! Do you think that there is a chance of integration with Androma? If so, please get in touch with viktor@androma.org

19 August, 2026 at 7:19 am

ygtisik

nice idea overall for setting a level. I work on whataifound.org to maintain a documented registry of AI usage and contributions in math and science. Palomar will definitely be something we integrate for data checks and validation.

19 August, 2026 at 8:17 am

Anonymous

Is there consideration of requiring or at least marking submissions that include a human readable explanation of the proof(which can be higher level than a normal paper since the proof is formalized alongside it). I’m concerned that the machinery behind them will become much less accessible for reuse.

19 August, 2026 at 8:27 am

Terence Tao

This registry is not designed to assess informal proofs (see item 3 of <https://palomar-registry.org/about#what-palomar-is-not>). However, we have no objection to having third-party services that build upon the registry to perform assessments of this type.

19 August, 2026 at 8:44 am

Lars Warren Ericson

How would you handle this repo with this arXiv writeup and this Lean proof code directory. It formalizes an entire paper which has multiple definitions and theorems. In general how would you approach Lean formalizations of whole papers, especially very long ones with hundred of results?

19 August, 2026 at 9:23 am

Terence Tao

We have a hard cap of 1000 lines (and 100KB) on the size of the challenge Lean file, which we very much want to keep human-readable (and AI-reviewable). (We in fact have a preference for challenge files that are significantly shorter than this hard cap, e.g., 300 lines.) For a large repository with multiple theorems which cannot all be stated in Lean within this cap, this would mean that multiple registry entries would be required to register separate statements for each major results.

If the results require extensive definitions to import that are not currently in Mathlib and whose constructions are too large to fit within the cap, then another option is to set up the required definitions in a Tau Ceti repository, which can then be imported as a dependency for the challenge file.

19 August, 2026 at 9:22 am

Anonymous

Do you think it is acceptable to register important results on Palomar before a preprint is submitted (while the writing is still in progress)?

19 August, 2026 at 9:47 am

Terence Tao

I have (reluctantly) come to the conclusion that authorship of the different stages of a proof development cycle – generation, verification, exposition, publication, and canonicalization – will become increasingly decoupled, that an author may be responsible for one part of this cycle but not be involved in another. In particular, much as we already normalize the submission of a preprint to a server such as the arXiv before formal publication, or the publication of paper before the definitive textbook containing the result is written, we will increasingly have to also permit the registration of formal proofs before a preprint is available. I do not view this decoupling of authorship as ideal, but it may be manageable as long as the incentives are such that the separate groups of authors can each be recognized for their particular contributions to the proof development cycle.

Palomar – a registry of Lean verified mathematics

Palomar – a registry of Lean verified mathematics

Palomar – a registry of Lean verified mathematics

Share this:

Recent Comments

Top Posts

Archives

Categories

The Polymath Blog

15 comments

Leave a comment Cancel reply

Comments (0)