About Palomar

What is Palomar?

Palomar is a public, searchable registry of Lean formalizations whose proofs have been machine-checked. Each entry points to an immutable version of a public repository and records the exact formal statement that was checked, its dependencies, the result of the proof check, and the findings of a documented editorial review.

Why do we need this today?

Formalized mathematics is growing quickly, but much of it remains scattered across repositories, announcements, and private links. A theorem that cannot be found, searched, cited, or inspected is much less useful than it could be. Palomar gives worthwhile formalizations a durable, indexable record organized around the mathematical result, not just the repository that happens to contain it.

Greater output—especially AI-assisted output—also makes a clear minimum standard more important. What Palomar checks, and what it does not, is set out below.

What does Palomar require for registration?

A repository version is registrable only after mechanical verification succeeds and an automated review identifies no blocking problem. The mechanical check uses both Lean’s kernel and the independent NanoDa kernel; the other checks are performed by a language model.

1. (Mechanical check) Comparator verifies that the recorded formal proof proves the recorded formal statement using a specified version of Mathlib, and that it uses only the axioms allowed by Palomar’s current Comparator configuration policy. This exported proof is replayed through both Lean’s kernel and the independent NanoDa kernel. The comparison is performed using the Comparator tool, which holds the advertised statement apart from its proof, so that a proof cannot quietly weaken the statement it claims to establish.
2. (Non-mechanical check) A language model judges that the recorded formal statement (conventionally Challenge.lean) is a fair rendering of the mathematical claim made in the recorded informal account. That account may appear in Challenge module documentation or declaration docstrings, the selected project README, or formalization.yaml, and the submission clears Palomar’s published minimum standard. That standard includes a floor on research interest, which requires the model to judge both of these to be answered yes:
   1. Could this result plausibly warrant a research paper or a serious research note?
   2. Can a credible research area be identified, together with a plausible kind of mathematician in a research department who could reasonably find the result interesting or relevant? No actual person need be named.
3. (Disclosure) The submission’s formalization.yaml records the required structured facts, including the project’s authorship, mathematical origin, sources or prior formalizations, automation methods, limitations, and review status. The narrative account may be supplied there or in the other eligible locations above. The same language model assesses whether the combined account is clear and adequately supported.

The checks the language model runs, the prompts it is given, and the report it must produce are published in PalomarPolicy.

All three checks run automatically. The review is a filter: it may identify a blocking problem, or it may find no blocking problem. It does not accept, approve, or endorse a result. Palomar adds no human editorial step: no one here reads the mathematics the way a referee would. When no blocking problem is identified, the submitter sees the private review and chooses whether to register or withdraw the result.

Palomar asserts nothing beyond these three checks.

For a registered result, the source and the review's comments are publicly visible, so that a reader can reach their own judgment on the work and verify it independently. The published review is redacted: it records that no blocking problem was identified and carries every comment, but not the scores behind them or how severe the review considered each one. The protocol specification defines what is published.

The scores behind that outcome are withheld deliberately. The same repository at the same commit has scored 5 and then 4 on one axis across two runs of the same policy, with the same registerability outcome both times, and a number that moves like that reads as a judgement it cannot carry. Readers are instead told whether the automated review identified any blocking problem.

I disagree with the review’s assessment of my result. What can I do?

There is no appeal for an individual result: reopening a few outcomes for whoever writes in would make the outcome depend on who complained. A rejected submission leaves no public record, and it can be revised and resubmitted after a waiting period. Repeated submissions lengthen that wait steeply, but carry no other penalty.

If you think the editorial floor itself is wrong, or you have run into anything else that looks like a defect in Palomar rather than a disagreement about one result, please raise it in the Palomar channel on the Lean Zulip.

What does the licence check cover?

Palomar records the root licence file, SPDX identifier, and checksum for the submitted repository at its pinned commit. This is not legal or ownership verification: cited papers, reused formalizations, and dependencies retain their own licences.

What happens to an entry when Lean or Mathlib is updated?

Nothing. Each entry verifies one immutable snapshot of a repository against the exact Lean toolchain and the exact dependency revisions that snapshot pinned, and the entry records these details. Palomar never re-runs a verified entry against a later Lean or Mathlib, so an entry neither improves nor decays as those projects move.

To record a result against newer versions, submit the updated commit and give the existing Palomar ID on the submission form. The new submission is verified and reviewed from scratch. If the automated review identifies no blocking problem and you choose to register it, it becomes the next version of that same identifier. The repository, project directory, and Comparator configuration path must match the existing entry.

Every version stays permanently resolvable at its explicit version URL, while an identifier on its own resolves to the newest active version.

What Palomar is not

1. Palomar’s formal certification is not absolute. As described in SECURITY.md, Palomar makes its best efforts to formally verify the claimed results in Lean in a secure, sandboxed environment. However, it is still possible that the version of the Lean kernel, Mathlib cache, and other tooling used by Palomar contains bugs or exploits. In particular, Palomar’s certification does not completely remove the need for independent verification of both the formal and informal proofs.
2. Palomar does not guarantee complete alignment of the formal and informal results claimed. The language model checks for any obvious discrepancies between the formal and informal versions of the result, and generates a detailed report of its findings. However, the model may make mistakes or have an incomplete analysis. This report is intended to assist the reader’s verification that the formal statement correctly captures the meaning of the informal one, but should not be viewed as a substitute for that verification.
3. Palomar does not verify informal proofs. Optionally, Palomar can check whether an informal account of a proof is consistent with the architecture of the formal proof, in that it does not describe an unrelated argument or conceal a decisive assumption. However, it does not re-derive or confirm the informal proof itself, and it makes no claim that an informal proof is correct.
4. Palomar does not assess code quality. While the formal statement file is audited for brevity and readability, formal proofs that are verified by Palomar are not assessed to be human readable, or to conform to any best practices for formal writing.
5. Palomar is not a certificate of novelty. Palomar does not check whether the results claimed are genuinely novel compared to what already exists in the published or unpublished literature.
6. Palomar is not a certificate of importance. Palomar applies a minimum editorial floor and rejects submissions that fall below it. Clearing that floor says only that a plausible research audience exists; Palomar does not rank, grade, or otherwise assess how significant a result is.
7. Palomar does not perform peer review. The automated checks above can block registration or identify no blocking problem; they do not accept a result, and no expert reviews the content of the repository itself.
8. Palomar is not a journal. Registration of a repository on this site should not in any way be viewed as a “publication” of that repository.
9. Palomar is not a green light for journal submission. Mathematical journals require their submissions to meet professional standards of exposition, accuracy, novelty, significance, and citation. Palomar addresses only limited aspects of these criteria: its automated review checks the informal account for clarity and fidelity, examines important citations, and applies a minimum research-interest floor. This is not a substitute for expert review of exposition, accuracy, novelty, or significance.
10. Palomar is not a green light for formalized library submission. Palomar verification should not be viewed as an endorsement of the code for the purposes of uploading to a library of formal proofs, such as Mathlib.
11. Palomar is a registry, not a repository. The mathematics stays in the original GitHub repository that is not Palomar’s and remains under its owner’s control; an entry records a claim about one commit of it rather than hosting the development. Palomar does keep a public preservation fork of every registered source, solely as a backup for the registry in the event that the original repository disappears.

Is there a way to leave comments on a registry entry?

Not on Palomar, which does not have the resources to moderate discussion.

The repository an entry points at is the natural home for technical discussion, and most accept issues and pull requests. Beyond that, the registry metadata is dedicated to the public domain under CC0 and published with feeds, so anyone can build a commentary layer over Palomar. However, Palomar does not run or endorse any such site.

How can I check this myself?

Every submission is pinned to a full 40-character commit, so the artifact Palomar checked cannot drift. Every verification runs in public GitHub Actions, but GitHub retains those workflow logs for only 90 days, so the log itself is not the durable record. Registered entries instead preserve the resulting mechanical report and workflow provenance with the append-only registry record. Those entries record the SHA-256 digest of the report and the exact workflow revision, alongside the statement and proof digests, Lean toolchain, and exact Comparator, lean4export, and Landrun revisions used, which together are enough to reproduce the run from the published record. One caveat: Mathlib’s build cache is fetched from a mutable store, so a later re-run may not retrieve identical artifacts. Building Mathlib from source removes that dependency.

Comparator does not simply ask Lean’s elaborator whether the proof was accepted. It compiles the statement and the proof in separate sandboxes, exports both environments with lean4export, checks that the declarations the statement depends on are identical in each. Palomar then requires the exported proof to be accepted from scratch by both Lean’s kernel and nanoda, an independent kernel implementation. A proof that survives those checks cannot have relied on a metaprogram tampering with the elaborator’s state or misreporting its result.

Comparator also enforces that the compared theorems use no axioms beyond those listed in the configured Comparator JSON file. Because that file is written by the submitter, Palomar validates it against the current Comparator configuration policy, including its axiom and independent-checker requirements, before Comparator runs.

Lean’s replay is a second pass rather than a second implementation: it guards against a proof that manipulated the elaborator, not against a bug in Lean’s kernel itself. Palomar therefore always requires nanoda as a genuinely independent check and publishes the exact NanoDa commit with every registry entry. We encourage readers to reproduce either check themselves:

• leanchecker replays every constant, imported and local, into a fresh environment (lake env leanchecker --fresh Module). It ships with every Lean toolchain Palomar supports, so it is already present in the toolchain each entry names. Like Comparator’s replay, it uses Lean’s own kernel.
• nanoda is an independent kernel implementation written in Rust. It does not share Lean’s kernel code, so it can catch a class of problem that neither Comparator’s replay nor leanchecker can.

The Lean reference manual’s guide to validating a Lean proof describes both, along with further checkers collected in the Lean Kernel Arena.

In addition to independently checking that the formal proof proves the formal statement, readers are also encouraged to compare the formal statement against the informal statement, and in particular to consider whether the definitions the statement relies on capture their intended informal meaning, for instance by handling degenerate cases correctly.

To assist with such comparisons, Palomar caps the size of the formal statement at 1,000 lines and 100 KiB. Imports are restricted to Lean core and pinned allowlisted libraries; the language model audits the definitions actually reached from those sources. Each registry entry displays the compared declarations, with their types available on hover, and links the exact statement file at the exact commit.

What external library imports are permitted?

The statement — conventionally Challenge.lean — may import Lean core, Mathlib, and Tau Ceti. Importing Tau Ceti is permitted and marks the entry as having qualified statement dependencies. A project Palomar has already registered is not importable on that basis.

The proof is not restricted this way: dependencies used only by the Solution may be arbitrary pinned Git repositories. The full rules are under what Comparator requires.

Who are we?

Palomar was initially incubated by the Lean FRO and ICARM. Palomar launches with three distinct groups, even though their initial memberships overlap. The complete role and access contract is maintained in Palomar Policy.

Technical Maintainers

Technical Maintainers can change Palomar's repositories, software, services, and deployed behaviour. The initial Technical Maintainers are Terence Tao, Matthew Ballard, Nestor Guillen, and Jaume de Dios.

Moderators

Moderators may authorize the exceptional retraction or restoration of one exact registered version. A Technical Maintainer executes the validated private-database change; canonical history is not erased. The initial Moderators are Jeremy Avigad, Matthew Ballard, Jaume de Dios, Nestor Guillen, Bryna Kra, Kim Morrison, Terence Tao, Ravi Vakil, and Akshay Venkatesh.

Scientific Advisory Board

The Scientific Advisory Board advises on policy, standards, and scientific direction. Board membership carries no operational duty or repository authority by itself, and the board does not review, approve, or endorse individual submissions. The initial board is Jeremy Avigad, Matthew Ballard, Jaume de Dios, Nestor Guillen, Bryna Kra, Kim Morrison, Terence Tao, Ravi Vakil, and Akshay Venkatesh.

These memberships may change as the project develops. Kim Morrison is the initial point of contact. Questions and proposals are welcome in the Palomar channel on the Lean Zulip.

What about other proof assistants?

Currently, Palomar is set up to verify only proofs formalized in Lean. However, we are open to expanding the registry to other proof assistants. If you are interested in such an expansion, please contact the maintainer team early in the Palomar channel on the Lean Zulip. We envisage that such expansions will require the following:

• pull requests adding support for the language, covering:
  • running its verification pipeline;
  • enforcing a separation between “the statement” and “the solution”;
  • rendering the main result to HTML; and
  • parsing upstream dependencies for display;
• a review, carried out with us, establishing that the implementation is secure and performant;
• an assessment of the resources its verification pipeline would require to run in our continuous integration;
• a sample of 10–100 candidate projects that could be indexed for that proof assistant; and
• someone ready to join its maintainer team.