Palomar – a registry of Lean verified mathematics

In recent months, there has been a surge of AI-generated proofs for various mathematical results, some of which have been formalized using the Lean proof assistant language. Checking whether a given Lean repository accurately proves the claimed statement can be challenging, particularly for those unfamiliar with Lean's usage. One must verify that the formal Lean statements typecheck correctly, contain no "cheats" like additional axioms, and accurately represent the informal descriptions of the results.

To address this issue, the Palomar registry of Lean verified mathematics has been launched, an initiative incubated by the Lean FRO and ICARM. The registry is open for submissions and is led by a team of experts, including Jeremy Avigad, Matthew Ballard, Jaume de Dios, Nestor Guillen, Bryna Kra, Kim Morrison, Ravi Vakil, and Akshay Venkatesh. The motivation behind Palomar is explained in detail on its dedicated page.

Palomar functions similarly to a preprint server, but for Lean proofs. It is a registry of external Github repositories, or snapshots of such repositories, containing formalized Lean code that adheres to best practices. When a snapshot of a repository is submitted to Palomar, it undergoes two checks. The first check, (a), is purely mechanical and uses the Lean tool Comparator to ensure the solution module typechecks and proves the exact results claimed in the challenge file.

The second check, (b), is non-deterministic and performed by a large language model, evaluating whether the informal description of the result in the formalization.yaml file matches the claimed result in the challenge file and if the repository meets minimal standards for entry.

If a repository passes both checks, it can be registered on Palomar. However, it is crucial to note that these checks fall short of a proper human peer review assessing novelty, interest, and accuracy, as Palomar is not a peer-reviewed journal. The submission process is thorough but achievable, as demonstrated by the author submitting their recent formalization of Sendov's conjecture to Palomar.

The registry accepts submissions of both old and new results, whether human-generated, AI-generated, or a combination of both. Before submitting, it is recommended to read the detailed instructions provided on the registry's instructions page. Discussion and feedback on Palomar can be found on the designated Zulip channel.