Palomar Opens Registry for Lean-Verified Mathematics

According to Palomar's documentation, a registrable repository version must pass a mechanical verification process and an automated editorial review without a blocking issue.

For the mechanical layer, Palomar records a formal challenge statement separately from its proof. Its Comparator tool checks that the proof establishes that recorded statement, rather than a weakened alternative. The exported proof is replayed by Lean's kernel and the independent NanoDa kernel, while the registry also checks that only axioms permitted by Palomar's current policy are used.

The registry's second layer is non-mechanical. Palomar states that a language model evaluates whether the formal statement is a fair rendering of the associated informal account, which can appear in project documentation, declaration docstrings, a README, or formalization.yaml. The review standard also includes a research-interest threshold, according to the registry's About page.

Tao's description of the expected repository structure identifies three core artifacts:

• •A challenge file containing a short, human-readable Lean description of the result claimed.
• •A solution module containing the formal proof.
• •A formalization.yaml file with an informal description, metadata, and disclosures.

Palomar's published process separates several questions that are often conflated in formal-mathematics announcements: whether Lean accepts a proof, whether the proof uses permitted axioms, whether it proves the advertised formal theorem, and whether that theorem reasonably corresponds to an informal claim. The first three are grounded in mechanical checks; the last is explicitly an LLM-mediated editorial judgment rather than a mathematical proof of semantic equivalence.

For researchers building AI systems for theorem proving, that distinction is material. Formal proof verification can establish properties of a precisely specified Lean statement, but model-generated prose can still overstate, underspecify, or mischaracterize the theorem being formalized. Registries with immutable repository references and explicit proof artifacts can make independent inspection, citation, and reproducibility easier across both human and AI-assisted formalization work.

Palomar's documentation describes the project as a registry of external GitHub repository snapshots, rather than a repository that hosts all underlying code itself. That design ties each registered claim to a specific source state, avoiding ambiguity when a public proof project later changes.