How to submit

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 source-repository example, see Erdős unit distance problem. To inspect registered examples and their exact recorded revisions, browse the current registry.

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:

• exactly one of lakefile.toml or lakefile.lean, with a committed lake-manifest.json required for lakefile.lean projects;
• lean-toolchain, pinned to a supported Lean release or release candidate (a repository-root file may be shared by a nested project, but a project-local file takes precedence);
• a small, readable Challenge module a mathematician should audit, conventionally Challenge.lean;
• a proved Solution module, conventionally Solution.lean;
• a Comparator JSON configuration, conventionally comparator.json, naming every theorem and definition Comparator should compare.

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 and may use deliberate sorry holes; the Solution module supplies the proved version. The proved Solution declarations must not depend on sorryAx, Lean.ofReduceBool, a custom axiom, or an unnamed missing definition. The compared declarations must have the same names and types. Comparator rebuilds and compares them, checks the permitted axioms, and verifies the proof. Palomar validates the submitted configuration against Palomar’s current mechanical requirements before verification.

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 permitted and marks the entry as having qualified statement dependencies. A project Palomar has already registered 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 permitted when their targets remain within the same pinned repository checkout. Neither kind relaxes the stricter transitive Challenge-import rule.

My formalization needs axioms beyond the standard set. Can it still be registered?

Not as axioms. A proved Solution declaration may depend only on the standard three Lean axioms: propext, Classical.choice, and Quot.sound. In particular, sorryAx and Lean.ofReduceBool, which sorry and native_decide introduce, are not permitted. Ordinary decide is fine. The Challenge module, by contrast, is expected to contain sorry.

If a result is conditional, state its hypotheses instead of assuming them, for instance writing theorem euler_product (h : RiemannHypothesis) : … instead of axiom RiemannHypothesis : …. With multiple hypotheses, a bundled typeclass can reduce boilerplate at use sites. It is better to write [LiteratureHypotheses] in each theorem signature that needs it than to declare it with variable, which can obscure which theorems use it.

What belongs in formalization.yaml?

The structured metadata must 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, what is original or adapted, the role of AI and human review, and any fidelity gaps, extra assumptions, or scope limitations. That narrative may be in formalization.yaml, Challenge module documentation or declaration docstrings, or the selected project README. Keep precise bibliographic references in the structured metadata. 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.

Use sources[].authors only for bibliographic authorship. To credit someone for another source role, use sources[].contributors; each contributor has a name and a free-form role, such as editor or problem proposer. The starter metadata shows the exact YAML shape. Palomar publishes these credits with the source and displays them on the registry entry.

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. Prove that you can write to the repository you are submitting. In a browser this is a GitHub sign-in: Palomar reads whether that account can push and then discards the token, keeping the account name in its private submission state.
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.

There are two ways to prove that write access, and they do not establish the same thing. A sign-in answers for one account: GitHub reports that this account can push, and the same account identified itself to Palomar. An agent has no browser, so it instead pushes a tag at the submitted commit and posts a gist carrying the same challenge. That establishes that someone who can write to the repository submitted it, and that an account named itself, which are not provably the same account. It is deliberately the weaker of the two, and Palomar's private submission record says which route a submission used; the public registry entry does not carry it. The protocol specification states the difference. Neither is proof of authorship, which is why you are asked about your relationship to the formalization separately.

What is public, and what is not

Public from verification onward: your repository, your commit, the submission identifier, the authorization relationship you declared, any approval evidence you wrote, and the identifier of the record you are correcting if you are correcting one. Mechanical verification runs in a public GitHub Actions workflow, and the inputs it was dispatched with are as public as its logs. Your notes are deliberately not among them. Whether you later register is inferable from the registry.

Not public unless you register: the automated review and its findings, and the registry record itself. If a review goes badly, or you simply change your mind, withdrawing leaves no public trace of either. The already-public verification run remains, and so does everything its inputs carried.

Not published whichever you choose: your identity as submitter. Palomar does not publish the GitHub account that proved push access, and the registry record has no field for the person who sent a submission. What a record carries about you is the authorization relationship you declared and, if you wrote one, the approval evidence you supplied, which is free text and is public. Your repository is public too, so the account that owns it stays as visible as it was before you submitted. What Palomar does not do is put your name in the record.

“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 the review outcome can be audited. Do not put anything sensitive in the notes field.

The privacy policy completes this: which field is kept where, how long each is retained, what withdrawing before registration scrubs and what it leaves behind, and how to ask for something to be corrected or taken down.

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.

If an operator or tool failure prevents the automated review from completing, the status page says review-failed. That is an operational fault, not a decision about the submission; Palomar can investigate and rerun it.

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

Nothing is registered until you ask for it. If the automated review identifies no blocking problem, your status page offers two choices: register, or withdraw. The automated review does not accept, approve, or endorse a result. Asking to register is how you authorise the record to be served, and it is the last point at which the choice is yours alone. The privacy policy explains that serving the record afterwards rests on Palomar's legitimate interests rather than on your consent, so withdrawing is not available once you have registered, and what you have instead is a further version or a request under the lawful-request process that policy describes. Registration is meant to be permanent: the record, the review, and your repository and commit enter Palomar's canonical history, which is append-only in ordinary operation. A named Moderator may exceptionally retract one exact version from the active public registry; that does not delete or rewrite the canonical record, and the public service retains a minimal tombstone. What that rule does not do is override a legal obligation Palomar is under, and the privacy policy describes the process by which one reaches the ledger. Identifying no blocking problem is not registration; a submission appears in the registry only after the corresponding database pull request is merged.

Corrections and dependency updates may be registered as new versions of the same Palomar ID, and every earlier version remains resolvable. A new mathematical result receives a new ID. A Palomar ID on its own resolves to the newest version of that record. 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.