Palomar – a registry of Lean verified mathematics

Summary

In recent months there has been a proliferation of AI-generated proofs of various old and new results, some of which have been formalized in the proof assistant language Lean. However, checking that a given Lean repository actually proves the claimed statement is somewhat non-trivial, especially for an audience which is not expert in the use of Lean: one has to first check that the claimed formal Lean statements have proofs that typecheck, that the proofs do not contain any “cheats” such as adding additional axioms, and that the formal statements also match (in a semantic sense) the informal description of the claimed results. To help bring some clarity to this situation, I am happy to announce that Palomar registry of Lean verified mathematics , which is an initiative incubated by the Lean FRO and by ICARM , is now open for submissions. I am serving in several roles on this registry, including on the scientific advisory board, together with Jeremy Avigad , Matthew Ballard , Jaume de Dios , Nestor Guillen , Bryna Kra , Kim Morrison , Ravi Vakil , and Akshay Venkatesh . A detailed motivation for Palomar can be found here , and further information about Palomar can be found here . A zeroth approximation of what Palomar intends to be is the analogue of a preprint server for Lean proofs. More precisely, Palomar (which is named after the astronomical observatory ) is a registry of external Github repositories (or more precisely, “snapshots” of such repositories, as represented by a specific Github commit) containing Lean code adhering to the current best practices for such formalizations, in particular containing A “challenge file” containing a short, human readable description in Lean of the results claimed. A “solution module” containing an (arbitrarily long) proof of the results claimed in the challenge file. A “ formalization.yaml ” file describing the results in informal language, and also containing a number of other relevant metadata and disclosures. (There are also some additional technical requirements for the repository which I will omit here.) If a snapshot of a repository is submitted to Palomar, it will check both (a) that the solution module typechecks and proves exactly the results claimed in the challenge file, and that (b) the informal description of the result in the formalization.yaml file appears to match the result claimed in the challenge f…