Registry of Lean verified mathematics
Related to mathematical verification and proof systems
Posted on Terry Tao’s blog

Palomar – a registry of Lean verified mathematics

What’s new

Updates on my research and expository papers, discussion of open problems, and other maths-related topics. By Terence Tao

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.

Like Loading…

The Polymath Blog

29 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.

20 August, 2026 at 6:13 am

Anonymous

This is not related to your project, but I have been considering implementing a standard that would formalize a bit this kind of process, pinning a claim to a computation. See claimpins.org.

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 a 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 written to professional standards is available. I do not view this decoupling of authorship as ideal – there are advantages to having a single group of authors be responsible for a proof throughout its development, much as there are advantages to having a single group of parents raise a child from conception to adulthood – but non-traditional authorship arrangements 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. (In particular, we may need a more explicit process to “hand off” the responsibility of authorship from one group to another in such cases.)

19 August, 2026 at 10:57 am

Anonymous

How likely is it that AI can start reading through textbooks and autoformalizing results by following the arguments line by line (possibly up to issues with canonicalizing with the current Lean library)? For example Stacks Project.

19 August, 2026 at 11:40 am

Terence Tao

There has been a very significant improvement in autoformalization capabilities in the last six months alone, at least if one focuses on the narrow goal of *only* certifying that a formal proof exists. I expect that (at least in some subfields of mathematics) a large fraction of textbooks and papers will soon be technically autoformalizable in that they can produce formalized versions of the statements of the main results of such texts, and provide typechecked proofs, though the proofs may not literally follow the informal proof “line by line” and may be inefficient, not human-readable, or otherwise not completely satisfactory in terms of code quality.

19 August, 2026 at 11:06 am

Anonymous

Terry, this is a very nice project!

I run a site called TheoremDB, which approaches some of the same questions from a different angle and may be of interest to you. I think there is a large engineering design space here that is worth exploring, so seeing how another site approaches the problem may yield some useful ideas for Palomar.

Some specific differences:

TheoremDB gives a theorem an identifier independent of any particular repository or Lean declaration, so several proofs, formalizations, computations, and failed attempts can be collected under the same statement. This separates “has this artifact been checked?” from “what is already known about this theorem?”

I am especially interested in what this permits for “negative traces.” Human mathematical literature preserves only a small fraction of this material. With machine mathematics, such traces can be produced as a routine by-product of search, stored systematically, and returned to the next agent before it repeats the same work. This gives us reusable research memory at a scale that was previously impractical. Here is an example packet; the underlying artifacts are in the Work tab.

TheoremDB exposes its agent workflow through MCP. Palomar organizes submission around a GitHub repository, so this gives agents a somewhat different way into the system. An agent can fetch the exact statement and previous work, check a private Lean draft, submit the exact source that passed, and later check its verification status. A Palomar MCP could plausibly expose its existing preflight and submission process in the same way. I also created a custom GPT as a ready-made client, making it easier to create entries with very little setup.

One further difference is repeated private checking before submission. Palomar already uses GitHub Actions for public verification. TheoremDB also keeps Lean environments ready for private draft checks, which makes iteration considerably faster. If Palomar eventually wanted this kind of draft lane, it could sit before the current public verification process.

Anyway, I think Palomar is a wonderful and rigorous initiative. There is a large engineering design space here, and I think it will be valuable to see several approaches explored.

19 August, 2026 at 4:00 pm

Anonymous

“The submission process is thorough, but achievable:”

This is AI.

19 August, 2026 at 4:43 pm

Terence Tao

Sorry to disappoint any AI detectives, but the text here was human-generated. (The use of a “but” after a comma (or the rhetorical device of antithesis in general) predates the advent of AI by several millennia, although AI models likely have trained extensively on that particular rhetorical pattern in the literature, most infamously in the “Not X, but Y” construction. But this does not justify affirming the consequent.)

As a side note, integrating AI workflows into WordPress directly currently requires more authorization of my AI agents over my computer than I am currently willing to grant, and I don’t see a major efficiency gain in delegating the writing of short blog posts like this to AI to be worth the various costs. I have managed however to use AI to improve Luca Trevisan’s old LaTeX to WordPress HTML converter Python script, which I now use for lengthier blog posts (for instance, my version of the script now handles images, which I previously had to input by hand); and it has also created a tool to semi-automatically repair mangled text in comments arising from the quirks in WordPress’s hybrid LaTeX/HTML parser.

(All uses of rhetorical antithesis in this comment were also human-generated.)

19 August, 2026 at 4:55 pm

Vinicius Rodrigues

Interesting project!

Last week we sucessfully used GPT-5.6 Sol to solve Wallace’s question, a 73 year old problem on the structure of topological groups and semigroups. We also produced a formal proof. This morning I submitted it to Palomar to try it out, and it was accepted in less than a hour. It will be interesting to see how the project evolves!

Cheers!

20 August, 2026 at 6:23 am

Anonymous

Is a one theorem to many formalizations, or perhaps simpler to manage one formalized theorem to many formalized proofs supported?

At some point, with a large enough database, it would be interesting to use the formalized proofs to study measures of quality. Some fuzzy and hard to define, like elegance, some more objective, like containing lemmas that are used in many other proofs. Perhaps the comparative study could detect lemmas, or proof patterns, which applicability has been overlooked.

20 August, 2026 at 10:19 am

Terence Tao

Palomar is organized around individual theorems that have a designated proof, although the proof itself is only checked to establish a type-identical statement to the claimed theorem, and no further analysis of the proof is provided. So a theorem with N different formal proofs would give more or less identical Palomar registry items. But I certainly agree that other qualities of formal proofs should be studied systematically; this is out of scope of this particular registry though.

20 August, 2026 at 6:31 am

Lars Warren Ericson

If a submission requires revision, e.g. for a metadata update, is the right workflow to push “Abandon this submission” for the prior submit after revising? The workflow available for revising a submission is for registered and accepted submissions, not new ones.

20 August, 2026 at 10:23 am

Terence Tao

Starting a new submission for the same repository automatically closes any previous open submissions, so it is not necessary to explicitly abandon the previous submission. (We don’t yet have a separate mechanism for updates that only change metadata, so unfortunately any such change will need to rerun comparator etc.)

20 August, 2026 at 11:08 am

Lars Warren Ericson

Today I registered bridge theorems between 3 presentations of Scott domain theory (lattices, information systems and neighborhoods). It took 3 tries. First it asked me to revise the bridge theorems. Then it said everything was OK but my metadata. I initially had one repo for 1972, 1980/81 and 1982 papers and then I split it into 3 because of complexity and then I wrote a 4th with the bridge theorems. The first 3 repos were formalisations and the bridge theorems I have not seen elsewhere. Formalization and novel get different keywords. I had to describe this provenance exactly right in the metadata. Then I submitted again and the reviewer engine failed to complete 2 times before succeeding. Finally I got the Register button. Which is awesome! But history of why each submit got changed is buried in the final inducted repo, which is OK but not as easy to track in your system if you want to look back and see for example what are the most common causes are of resubmit. Also, versus an earlier comment, getting the bridge theorems accepted is in a way a hack that gets the underlying formalizations into the system. All told around 90,000 lines of Lean code. But the bridge theorems under 400!

21 August, 2026 at 10:02 am

Anonymous

This project makes me realize that at some point in the coming crisis, all our papers and books will probably get autoformalized. It would be not great if it happens in a complete chaos. I am not super happy with the idea of having anyone (or several people) autoformalizing my papers and their machines possibly finding mistakes. Ideally I would prefer having a colleague trying to understand it and possibly pointing mistakes (but let’s be realistic: my existing papers get seriously read by maybe 2-3 people so far, and it will not get better with the flood, though I have had the chance to have some serious referees on a few past occasions). So it’s not inconceivable to put them here (if co-authors agree), knowing that it’s at least managed by the community. Let me specify that I am not at all an AI-enthusiast, much to the contrary, neither a supporter of autoformalization, and I am not willing to contribute myself in the coming flood by using LLMs.

21 August, 2026 at 12:01 pm

Lars Warren Ericson

The Palomar registration function is broken. I have a validated submission that is stuck waiting for operator attention since 2026-08-20T18:44:33Z. I put a note on the Zulip Palomar channel: #Palomar > Registration queue jammed @ 💬

For commenters

To enter in LaTeX in comments, use $latex __$ (without the < and > signs, of course; in fact, these signs should be avoided as they can cause formatting errors). Also, backslashes \\ need to be doubled as \\\\. See the [about page](https://terrytao.wordpress.com/about/) for details and for other commenting policy.

« A digestion of the proof of Sendov’s conjecture

Quantitative bounds for sets lacking polynomial progressions with shifted prime difference »

Blog at WordPress.com.Ben Eastaugh and Chris Sternal-Johnson.

Subscribe to feed.

Comment
Reblog
Subscribe Subscribed
- What’s new
Join 12,333 other subscribers

Sign me up
- Already have a WordPress.com account? Log in now.
- What’s new
- Subscribe Subscribed
- Sign up
- Log in
- Copy shortlink
- Report this content
- View post in Reader
- Manage subscriptions
- Collapse this bar

Palomar

Palomar – a registry of Lean verified mathematics

Recent Comments

Top Posts

Archives

Categories

The Polymath Blog

29 comments

Leave a comment Cancel reply

For commenters

Highlights & notes

Notes

Palomar

Palomar – a registry of Lean verified mathematics

Share this:

Recent Comments

Top Posts

Archives

Categories

The Polymath Blog

29 comments

Leave a comment Cancel reply

For commenters

Highlights & notes

Notes