Palomar

About Palomar

What the registry does, what it means, and how to submit

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 acceptance by Palomar mean?

In order for a repository version to be accepted into the Palomar registry, three checks must pass. One is mechanical and requires both Lean’s kernel and the independent NanoDa kernel; the other two 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 depends on no axioms beyond propext, Quot.sound, and Classical.choice. 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 statement (in formalization.yaml), and that 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 states the project’s authorship, mathematical origin, any sources or prior formalizations, automation methods, limitations, and review status explicitly, rather than leaving them to be inferred. The same language model assesses whether that account is clear and adequately supported.

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

All three checks run automatically, and a submission that passes them is published without further judgment. Palomar adds no human editorial step: no one here reads the mathematics the way a referee would.

Palomar asserts nothing beyond these three checks.

The source, warnings, and full review of the repository are publicly visible to help readers reach their own judgment on the work and perform independent verification.

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 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. Acceptance is decided by the automated checks above, 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 adhere to professional standards of exposition, accuracy, and citation, and be of genuine interest to their readers. None of these criteria are directly addressed by this registry, which checks informal descriptions of results only for fidelity to their formal counterparts.
  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.

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. Entries published under the durable-evidence schema (version 5) 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 separately rejects any submission whose list extends beyond propext, Quot.sound, and Classical.choice.

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 enables nanoda as a genuinely independent check and publishes the exact NanoDa commit with every registry entry. We encourage readers to reproduce either check themselves:

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.

Getting ready to submit

Start with a public GitHub repository and choose the exact commit you want Palomar to review. The commit must be identified by its full 40-character SHA (the unique hash Git assigns to it).

Using Git, commit and push every change you want included. In a terminal in the repository folder, run git rev-parse HEAD and copy the entire 40-character result. Uncommitted changes are excluded.

Using GitHub, click the commits link above the repository’s file list. Find the commit and click the clipboard icon beside its shortened hash (“Copy the full SHA”). Palomar can fetch only commits pushed to the public repository. It checks that immutable snapshot, not a branch or tag that can change.

The Palomar starter repository provides this layout, pinned dependencies, documentation generation, CI checks for Lean and Comparator, and a documented formalization.yaml starting point.

For a complete public example, see the source repository for Palomar’s first registered result.

The repository root is the default project directory, so the usual layout requires no path settings. If the Lean project lives in a subdirectory, enter that repository-relative project path on the submission form. You may also enter paths for a non-default Comparator configuration or formalization.yaml; omitted fields keep the conventional defaults inside the selected project.

The selected project directory must contain:

The required formalization.yaml describes the project, result, sources, authorship, automation, review, and known limitations. An explicit repository-relative path may keep it outside a selected nested Comparator project.

A committed manifest is strongly recommended. For a lakefile.toml project without one, Palomar can construct a trusted manifest only from contained path dependencies whose targets have committed manifests and no further path dependencies; other layouts must commit the selected project's lake-manifest.json.

Comparator may name safe dotted Challenge and Solution modules, and Palomar resolves their source files through the selected Lake project. The one conventional licence file remains at repository root even for a nested project, because the recorded licence covers the submitted repository snapshot.

What does Comparator require?

The Challenge module states the result independently, normally with sorry; the Solution module supplies the proved version. Their compared declarations must have the same names and types. Comparator rebuilds and compares them, checks the permitted axioms, and verifies the proof. Palomar currently permits only propext, Quot.sound, and Classical.choice.

Keep the Challenge source short and mathematically ordinary. 1,000 lines and 100 KiB are hard limits; 300 lines and 32 KiB is the surface we would rather review. Its transitive imports must resolve to Lean core or the pinned, allowlisted Mathlib or Tau Ceti closure, and to nothing else. Importing Tau Ceti is accepted and marks the entry as having qualified statement dependencies. A project Palomar has already accepted is not importable on that basis: an entry fixes a reviewable snapshot of its own statement, not a library for later submissions.

Dependencies used only by the Solution may be arbitrary pinned Git dependencies. Local/path dependencies are also accepted when their targets remain within the same pinned repository checkout. Neither kind relaxes the stricter transitive Challenge-import rule.

What belongs in formalization.yaml?

At minimum, include the project name, authors, license, and responsible maintainers; say whether the result is original or source-based and whether the repository is the substantive development or a thin Comparator wrapper; include one or two classifications from the arXiv category taxonomy and one to eight codes from MSC2020; the automation methods used (including manual, when appropriate); and the review status. For editorial review, also give a plain-language account of every compared theorem, precise bibliographic references, what is original or adapted, the role of AI and human review, and any fidelity gaps, extra assumptions, or scope limitations. Follow the formalization.yaml standard and Palomar’s submission policy.

A source may be a book, journal article, non-arXiv preprint, web discussion, private communication, or folklore; give the most stable reference available. A formalization that first presents a new result may have no source at all. If sources exist, state whether the project formalizes, adapts, independently proves, or merely uses each as background. Record prior formalizations separately. A thin wrapper must identify the substantive formalization repository at an immutable commit.

Submit only if you are a responsible author or maintainer of the substantive formalization, or have approval from one. For a thin wrapper this means the people responsible for the underlying formalization, not merely the wrapper repository. The submission form asks which applies; a link or note documenting approval is optional.

How to submit

  1. Push the final snapshot to a public GitHub repository and copy its full 40-character commit SHA.
  2. Open the submission form. Enter the repository and commit SHA. Leave the optional project, Comparator-config, and metadata paths blank for the normal root layout; fill them only for a nested or non-default layout. Record whether you maintain the substantive formalization or have approval from someone who does, and, for a correction to an existing entry, enter its Palomar ID.
  3. Sign in with GitHub so Palomar can confirm you have write access to the repository you are submitting. The sign-in is used once and is not stored.
  4. Keep the status page you are given. Its link is the only way back to your submission: Palomar does not email, and there is no account to sign in to.

What is public, and what is not

Public from the moment you submit: your repository and commit. Mechanical verification runs in a public GitHub Actions workflow, and its logs are public. Whether you later publish is inferable from the registry.

Not public unless you publish: the editorial review, the decision, and your identity as submitter. If a review goes badly, or you simply change your mind, withdrawing leaves no public trace of the review or the decision, and there is nothing for anyone to find.

“Private” here means not public, not confidential. Reviews are readable by Palomar operators, by GitHub, and by the model provider, and are retained indefinitely so that any decision can be audited. Do not put anything sensitive in the notes field.

What happens next

Your status page shows mechanical verification first, with a link to the public run. If verification fails, the report explains what failed. If it passes, the submission waits for editorial review; once mechanical verification has passed we aim to complete that review within one hour, though that is a target rather than a guarantee, especially when a submission needs specialist judgment.

The review then appears on your status page, and nowhere else. It gives the reasons, warnings, and any requested changes, not just a decision. A request for changes means the work may be reconsidered after specific correctable problems are addressed; a rejection means the submission failed a fundamental mechanical or editorial requirement; an escalation means specialist or human judgment is needed. Because every review is tied to an immutable commit, revised source is a new submission at a new full commit SHA.

Nothing is published until you ask for it. If the review is an acceptance, your status page offers two choices: publish, or withdraw. Publishing is permanent: the record, the review, and your repository and commit go into the public registry, and Palomar records are append-only, so a published record is never removed. Acceptance is not publication; an accepted submission appears in the registry once the corresponding database pull request is merged.

Corrections are published as new versions of the same Palomar ID, and every earlier version remains resolvable. A Palomar ID on its own resolves to the newest version of that record, and a later version may change the theorem, source, authors, or subject radically. For a stable citation, name the version (e.g., PALOMAR-2026-07-29-000001 v1 instead of PALOMAR-2026-07-29-000001). The entry page URL always names the version you are viewing, so copying it from the address bar gives a citable link.

Who are we?

Palomar was initially incubated by the Lean FRO and ICARM. The initial Scientific Advisory Board is Kim Morrison, Nestor Guillen, Terence Tao, Akshay Venkatesh, Jeremy Avigad, Bryna Kra, Ravi Vakil, Jaume de Dios, and Matthew Ballard. The board advises on policy and standards; it does not review, approve, or endorse individual submissions. The board, maintainer team, and project governance are expected to 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:

Ready to submit?

The form asks for a repository and one fixed commit.

Open the submission form