Palomar Opens a Lean Registry That Checks Proofs and Their Descriptions
The launch creates a fixed, inspectable record for formal proofs, but its automated checks leave questions of novelty, mathematical significance and expert review outside the registry.
Story brief
3 key pointsPalomar’s registry gives researchers a reproducible way to inspect Lean proofs while keeping formal verification separate from interpretation. Each entry points to an immutable GitHub commit, and Comparator checks whether the proof establishes the encoded theorem. A language model separately screens the prose description and repository, but Palomar treats that review as provisional. The registry accepts human-, AI-,...
- 01
Submissions opened August 18; Terence Tao is one of Palomar’s four initial technical maintainers.
- 02
Each entry includes Challenge.lean, Solution.lean and formalization.yaml, separating theorem, proof and description.
- 03
Comparator verifies the formal proof against the encoded challenge, not whether the encoding captures the intended mathematics.
Palomar has opened a public registry for Lean proof repositories, giving each registered submission a specific GitHub commit to inspect. It separates two questions that can easily blur together: whether code proves a formal statement, and whether an ordinary-language description appears to match that result. [claim-1, claim-2, claim-3]
Submissions opened on August 18. Terence Tao announced the launch and is one of Palomar’s four initial technical maintainers; the project was incubated by the Lean Focused Research Organization and the Institute for Computer-Aided Reasoning in Mathematics. [claim-4, claim-5]
One submission, three files
A Palomar submission includes three components. Challenge.lean states the formal result being claimed. Solution.lean contains the proof. formalization.yaml supplies an informal description, metadata and disclosures. Together, those files make the claimed theorem, its formal proof and its plain-language account available as separate objects for review. [claim-6, claim-7]
The registry records an external GitHub repository snapshot identified by a particular commit. That gives a reader a defined version of the submission to examine, rather than an evolving repository whose contents may change after registration. Palomar currently supports Lean and accepts submissions produced by people, AI systems or a mixture of both. [claim-1, claim-8, claim-9]
The mechanical test comes first
Palomar uses Comparator for the mechanical step. The tool checks whether the solution establishes the result stated in the challenge file. Its scope is deliberately formal: it asks whether this proof establishes this encoded statement, not whether the statement captures every meaning a mathematician may attach to a theorem described in prose. [claim-2, claim-10]
The second check addresses that gap, but only provisionally. A large language model evaluates whether the informal description appears to match the formal result and whether the repository meets Palomar’s minimum standards. Palomar warns that language-model review can miss discrepancies, so the screen is not a finding that prose and formalization genuinely coincide. [claim-3, claim-11]
A bounded answer to an AI-era problem
Tao framed Palomar as a response to a proliferation of AI-generated proofs, including work formalized in Lean. A proof checker can establish that code proves a proposition under its encoded assumptions. Readers still need to judge whether the definitions, assumptions and formal statement correspond to the mathematical result being presented in ordinary language. [claim-10]
That boundary is the point of the registry, not a flaw it tries to conceal. Palomar supplies a traceable artifact: a pinned repository version, a stated challenge, a solution and an account of what the work is meant to show. The result is material that other researchers can inspect and challenge, while the harder work of mathematical judgment remains outside registration. [claim-7, claim-13]