Palomar

Submit a Lean-verified result

Palomar verifies an immutable snapshot of a public repository, and performs a basic AI check that the formal and informal statements match and that the result is plausibly interesting to some mathematician. Read the submission policy first.

What is public, and what is not

The fact that this repository and commit have been submitted is permanently and publicly recorded. Your identity, the review, and the decision will not be public until you have seen them and decided to go ahead with registration.

The reviews are not completely secret prior to registration: they may be audited and acted on by the Palomar moderation team.

A public GitHub repository, as owner/name or a URL.

A full 40-character SHA. Branches and tags move; a record must not.

Your relationship to this formalization

If this repository is only a thin wrapper around another formalization, answer about that underlying repository, not the wrapper.

Registered permanently and cannot be withdrawn. Do not name anyone who has not agreed to be named.

Only to register a new version of a result already in the registry.

Read by the reviewer and kept with the private record. Do not put anything sensitive here.

You will be asked to sign in so Palomar can confirm you have write access to the repository you are submitting. The sign-in is used once and not stored.