Palomar: Lean Verified Math Registry

As AI-generated mathematical proofs surge, it has become crucial to verify whether these proofs accurately demonstrate what they intend to. To address this, the Palomar registry, led by Lean FRO and ICARM, has been officially launched.

Palomar operates by registering specific commits (snapshots) from external GitHub repositories, requiring the following three elements for registration:

• Challenge file: A human-readable short description of the result
• Solution module: Proof code for the result
• formalization.yaml: Informal description and metadata for the result

Registered repositories undergo a two-step verification process:

1. Mechanical verification: Uses the Lean tool Comparator to confirm that the solution module accurately proves the result stated in the challenge file.
2. Non-deterministic verification: Utilizes Large Language Models (LLMs) to check if the informal description in formalization.yaml matches the content of the challenge file.

Palomar is not a peer-reviewed journal that assesses academic novelty, but it serves as infrastructure to ensure the reliability of mathematical proofs generated by both AI and humans.