Palomar opens as a registry for Lean-verified math proofs
AI models have produced a growing wave of formal proofs written in the Lean proof assistant, covering both old and new results. Checking that a given Lean repository actually proves what it claims is not trivial, especially for someone who does not use Lean: it requires confirming that the formal statements typecheck, that the proof contains no "cheats" such as smuggled-in extra axioms, and that the formal statement actually matches the informal description of the result.
To address this, Palomar, a registry of Lean-verified mathematics incubated by the Lean FRO and by ICARM, is now open for submissions. The post's author serves on its scientific advisory board together with eight other named mathematicians: Jeremy Avigad, Matthew Ballard, Jaume de Dios, Nestor Guillen, Bryna Kra, Kim Morrison, Ravi Vakil, and Akshay Venkatesh. Palomar is described as a rough analogue of a preprint server for Lean proofs: a registry of external GitHub repositories, represented as snapshots at a specific commit, that follow current best practices for formalization.
A submission needs a "challenge file" with a short, human-readable Lean description of the claimed result; a "solution module" containing an arbitrarily long proof of that result; and a "formalization.yaml" file describing the result in informal language along with other metadata and disclosures. The author notes there are further technical requirements for the repository that the post does not spell out. Two checks then gate entry: a purely mechanical check, run with the Lean tool Comparator, that the solution module typechecks and proves exactly what the challenge file claims; and a non-deterministic check, performed by a large language model, that the informal description in formalization.yaml matches the formal claim. A repository that passes both, plus minimal registry standards, gets registered. The author is explicit that both checks fall well short of a proper human peer review for novelty, interest, and accuracy, and states plainly that Palomar is not a peer-reviewed journal.
As a test of the process, the author submitted his own recent formalization of the proof of Sendov's conjecture and got it through, calling the submission process thorough but achievable; he plans to submit older formalizations as well. The registry is open to old and new results alike, and to submissions that are human-generated, AI-generated, or a mixture of both. Detailed submission instructions are linked from the announcement, and the author adds that modern AI agents are quite helpful with the mechanical parts of preparing a submission, though a human review is still strongly recommended. Discussion and feedback on Palomar are directed to a dedicated Zulip channel.
Key facts
- Palomar, incubated by the Lean FRO and ICARM, is now open for submissions of Lean-verified mathematics proofs.
- Its scientific advisory board includes the post's author alongside Jeremy Avigad, Matthew Ballard, Jaume de Dios, Nestor Guillen, Bryna Kra, Kim Morrison, Ravi Vakil, and Akshay Venkatesh.
- A submission requires a challenge file (the claim in Lean), a solution module (the proof), and a formalization.yaml file (an informal description plus metadata).
- Entry is gated by two checks: a mechanical typecheck via the Lean tool Comparator, and a non-deterministic check by a large language model that the informal description matches the formal claim.
- As a test, the author submitted his own formalization of Sendov's conjecture; the author stresses that neither check amounts to peer review and that Palomar is not a peer-reviewed journal.
Why it matters
AI systems have been generating a growing number of Lean-formalized proofs of both old and new results, but verifying that a given Lean repository actually proves its claim is hard for anyone who does not already use Lean. Someone has to confirm the formal statement typechecks without hidden extra axioms and that it genuinely matches the informal claim being made. Palomar, incubated by the Lean FRO and ICARM, is meant to be a rough analogue of a preprint server for Lean proofs: a registry of vetted GitHub repository snapshots that a mathematician can point to, rather than an unsorted pile of unverified repos.
Who it affects
Mathematicians formalizing results in Lean, whether by hand, with AI assistance, or some mixture, gain a place to register a checked snapshot of their work rather than relying on an unvetted GitHub link. The registry's scientific advisory board is made up of the post's author together with Jeremy Avigad, Matthew Ballard, Jaume de Dios, Nestor Guillen, Bryna Kra, Kim Morrison, Ravi Vakil, and Akshay Venkatesh. Readers who want to check a claimed formal proof also benefit: a Palomar entry gives them a faster way to gauge whether it holds up, without having to read the Lean code themselves.
How to use it
A submission is a specific GitHub commit that must contain a challenge file with a short, human-readable Lean statement of the result; a solution module with the arbitrarily long proof; and a formalization.yaml file describing the result informally along with other metadata and disclosures. The author notes there are additional technical requirements for the repository that the announcement does not detail, and points readers to fuller submission instructions linked from the post. Modern AI agents, the author adds, are quite helpful with the mechanical parts of preparing a submission, though a human review is still strongly recommended. Discussion and feedback happen on a dedicated Zulip channel.
How solid is it
Two checks gate registration. The first is purely mechanical: the Lean tool Comparator confirms the solution module typechecks and proves exactly the statement made in the challenge file. The second is non-deterministic: a large language model checks whether the informal description in formalization.yaml matches the formal claim. As a trial run, the author submitted his own recent formalization of the proof of Sendov's conjecture and got it through the process, describing the submission process as thorough but achievable, and plans to submit older formalizations of his own as well.
Risks and caveats
The author is explicit that both checks fall well short of what a proper human peer review of a submission for novelty, interest, and accuracy would give, and states directly that Palomar is not a peer-reviewed journal. Passing the two checks confirms the proof typechecks and that a language model judged the informal description a plausible match; it does not certify that the result is new, important, or described without nuance lost. The announcement does not say how many submissions or repositories have been registered so far, nor what happens to a submission that fails either check.
“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.”
— the post's author, announcing Palomar