Palomar Opens a Lean Registry That Checks Proofs and Their Descriptions

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.

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.

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.

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.

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.

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.

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.

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.